Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions:
df-bi 206 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfbidf
2217 drex2
2441 rexbida
3269 rexeqfOLD
3351 opabbid
5213 zfrepclf
5294 dfid3
5577 oprabbid
7473 axrepndlem1
10586 axrepndlem2
10587 axrepnd
10588 axpowndlem2
10592 axpowndlem3
10593 axpowndlem4
10594 axregnd
10598 axinfndlem1
10599 axinfnd
10600 axacndlem4
10604 axacndlem5
10605 axacnd
10606 opabdm
31835 opabrn
31836 pm14.122b
43172 pm14.123b
43175 |