Colors of
variables: wff
setvar class |
Syntax hints: Ⅎwnfc 2885 class class class wbr 5103
{copab 5165 ◡ccnv 5630 |
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-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-cnv 5639 |
This theorem is referenced by: nfrn
5905 nfpred
6256 nffun
6521 nff1
6733 nfsup
9383 nfinf
9414 gsumcom2
19743 ptbasfi
22916 mbfposr
25000 itg1climres
25063 funcnvmpt
31469 nfwsuc
34263 aomclem8
41326 rfcnpre1
43166 rfcnpre2
43178 smfpimcc
44981 |