Colors of
variables: wff set class |
Syntax hints:
= wceq 1353 Ⅎwnfc 2306 |
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 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 df-cleq 2170 df-clel 2173 df-nfc 2308 |
This theorem is referenced by: nfrab1
2656 nfrabxy
2657 nfdif
3256 nfun
3291 nfin
3341 nfpw
3588 nfpr
3642 nfsn
3652 nfop
3794 nfuni
3815 nfint
3854 nfiunxy
3912 nfiinxy
3913 nfiunya
3914 nfiinya
3915 nfiu1
3916 nfii1
3917 nfopab
4071 nfopab1
4072 nfopab2
4073 nfmpt
4095 nfmpt1
4096 repizf2
4162 nfsuc
4408 nfxp
4653 nfco
4792 nfcnv
4806 nfdm
4871 nfrn
4872 nfres
4909 nfima
4978 nfiota1
5180 nffv
5525 fvmptss2
5591 fvmptssdm
5600 fvmptf
5608 ralrnmpt
5658 rexrnmpt
5659 f1ompt
5667 f1mpt
5771 fliftfun
5796 nfriota1
5837 riotaprop
5853 nfoprab1
5923 nfoprab2
5924 nfoprab3
5925 nfoprab
5926 nfmpo1
5941 nfmpo2
5942 nfmpo
5943 ovmpos
5997 ov2gf
5998 ovi3
6010 nfof
6087 nfofr
6088 nftpos
6279 nfrecs
6307 nffrec
6396 nfixpxy
6716 nfixp1
6717 xpcomco
6825 nfsup
6990 nfinf
7015 nfdju
7040 caucvgprprlemaddq
7706 nfseq
10454 nfsum1
11363 nfsum
11364 nfcprod1
11561 nfcprod
11562 lgseisenlem2
14421 |