Colors of
variables: wff
setvar class |
Syntax hints: e. wcel 1757 A. wral 2792
cvv 3052
C_ wss 3410 U_ ciun 4253 (class class class)co 6174
cmap 7298
X_ cixp 7347 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671
ax-6 1709 ax-7 1729 ax-8 1759
ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-rep 4485 ax-sep 4495 ax-nul 4503 ax-pow 4552 ax-pr 4613 ax-un 6456 |
This theorem depends on definitions:
df-bi 185 df-or 370
df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-eu 2263 df-mo 2264 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-ral 2797 df-rex 2798 df-reu 2799 df-rab 2801 df-v 3054 df-sbc 3269 df-csb 3371 df-dif 3413 df-un 3415 df-in 3417 df-ss 3424 df-nul 3720 df-if 3874 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4174 df-iun 4255 df-br 4375 df-opab 4433 df-mpt 4434 df-id 4718 df-xp 4928 df-rel 4929 df-cnv 4930 df-co 4931 df-dm 4932 df-rn 4933 df-res 4934 df-ima 4935 df-iota 5463 df-fun 5502 df-fn 5503 df-f 5504 df-f1 5505 df-fo 5506 df-f1o 5507 df-fv 5508 df-ov 6177 df-oprab 6178 df-mpt2 6179 df-map 7300 df-ixp 7348 |