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
3150 rabn0m
3452 nfdisjv
3994 nfdisj1
3995 nfpo
4303 nfso
4304 nfse
4343 nffrfor
4350 nffr
4351 nfwe
4357 nfrel
4713 sb8iota
5187 nffun
5241 nffn
5314 nff
5364 nff1
5421 nffo
5439 nff1o
5461 nfiso
5809 nfixpxy
6719 |