Colors of
variables: wff set class |
Syntax hints:
wb 105
wnf 1460 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 |
This theorem is referenced by: nfnf1
1544 nf3an
1566 nfnf
1577 nfdc
1659 nfs1f
1780 nfsbv
1947 nfeu1
2037 nfmo1
2038 sb8eu
2039 nfeu
2045 nfnfc1
2322 nfnfc
2326 nfeq
2327 nfel
2328 nfabdw
2338 nfne
2440 nfnel
2449 nfra1
2508 nfre1
2520 nfreu1
2649 nfrmo1
2650 nfss
3149 rabn0m
3451 nfdisjv
3993 nfdisj1
3994 nfpo
4302 nfso
4303 nfse
4342 nffrfor
4349 nffr
4350 nfwe
4356 nfrel
4712 sb8iota
5186 nffun
5240 nffn
5313 nff
5363 nff1
5420 nffo
5438 nff1o
5460 nfiso
5807 nfixpxy
6717 |