Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2104
∅c0 4262 dom cdm 5596
⟶wf 6450 ‘cfv 6454 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pr 5361 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3287 df-v 3439 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-opab 5144 df-id 5496 df-xp 5602 df-rel 5603 df-cnv 5604 df-co 5605 df-dm 5606 df-rn 5607 df-iota 6406 df-fun 6456 df-fn 6457 df-f 6458 df-fv 6462 |
This theorem is referenced by: harcl
9358 cantnfvalf
9463 rankon
9593 cardon
9742 alephon
9867 ackbij1lem13
10030 ackbij1b
10037 ixxssxr
13133 sadcf
16201 smupf
16226 iccordt
22406 nodense
33936 bdayelon
34012 madessno
34085 oldssno
34086 newssno
34087 |