Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 /\ wa 369
= wceq 1395 E. wex 1612 F/ wnf 1616
e. wcel 1818 F/_ wnfc 2605 |
This theorem is referenced by: nfel
2632 nfneld
2801 nfrald
2842 ralcom2
3022 nfreud
3030 nfrmod
3031 nfrmo
3033 nfsbc1d
3345 nfsbcd
3348 sbcrextOLD
3409 sbcrext
3410 nfdisj
4434 nfbrd
4495 nfriotad
6265 nfixp
7508 axrepndlem2
8989 axrepnd
8990 axunnd
8992 axpowndlem2
8994 axpowndlem2OLD
8995 axpowndlem3
8996 axpowndlem3OLD
8997 axpowndlem4
8998 axpownd
8999 axregndlem2
9001 axinfndlem1
9004 axinfnd
9005 axacndlem4
9009 axacndlem5
9010 axacnd
9011 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-an 371
df-ex 1613 df-nf 1617 df-cleq 2449 df-clel 2452 df-nfc 2607 |