Lines Matching refs:f7
2950 (!Z X. member(Z,second(X)) ==> little_set(f7(Z,X))) /\
2951 (!Z X. member(Z,second(X)) ==> equal(X,ordered_pair(f6(Z,X),f7(Z,X)))) /\
2952 (!Z X. member(Z,second(X)) ==> member(Z,f7(Z,X))) /\
3081 (!G8 H8 I8. equal(G8,H8) ==> equal(f7(G8,I8),f7(H8,I8))) /\
3082 (!J8 L8 K8. equal(J8,K8) ==> equal(f7(L8,J8),f7(L8,K8))) /\
3312 (!Vf X. equal_sets(union_of_members(Vf),X) ==> basis(X,Vf) \/ element_of_set(f7(X,Vf),X)) /\
3315 (!X Vf. equal_sets(union_of_members(Vf),X) ==> basis(X,Vf) \/ element_of_set(f7(X,Vf),intersection_of_sets(f8(X,Vf),f9(X,Vf)))) /\
3316 (!Uu9 X Vf. equal_sets(union_of_members(Vf),X) /\ element_of_set(f7(X,Vf),Uu9) /\ element_of_collection(Uu9,Vf) /\ subset_sets(Uu9,intersection_of_sets(f8(X,Vf),f9(X,Vf))) ==> basis(X,Vf)) /\