Colors of
variables: wff
set class |
Syntax hints: -> wi 4 /\ wa 360
A. wal 1556 e. wcel 1724 Tr wtr 4395
chf 26943 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1562 ax-4 1573 ax-5 1636
ax-6 1677 ax-7 1697 ax-8 1726
ax-9 1728 ax-10 1743 ax-11 1748 ax-12 1760 ax-13 1947 ax-ext 2462 ax-rep 4413 ax-sep 4423 ax-nul 4431 ax-pow 4477 ax-pr 4538 ax-un 6338 ax-reg 7672 ax-inf2 7708 |
This theorem depends on definitions:
df-bi 179 df-or 361
df-an 362 df-3or 940 df-3an 941 df-tru 1337 df-ex 1558 df-nf 1561 df-sb 1669 df-eu 2309 df-mo 2310 df-clab 2468 df-cleq 2474 df-clel 2477 df-nfc 2606 df-ne 2646 df-ral 2756 df-rex 2757 df-reu 2758 df-rab 2760 df-v 3008 df-sbc 3213 df-csb 3314 df-dif 3356 df-un 3358 df-in 3360 df-ss 3367 df-pss 3369 df-nul 3661 df-if 3813 df-pw 3880 df-sn 3900 df-pr 3901 df-tp 3902 df-op 3903 df-uni 4102 df-int 4139 df-iun 4183 df-br 4303 df-opab 4361 df-mpt 4362 df-tr 4396 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4850 df-rel 4851 df-cnv 4852 df-co 4853 df-dm 4854 df-rn 4855 df-res 4856 df-ima 4857 df-iota 5380 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-om 6442 df-recs 6745 df-rdg 6780 df-er 7017 df-en 7222 df-dom 7223 df-sdom 7224 df-r1 7802 df-rank 7803 df-hf 26944 |