Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1541 ∈ wcel 2106
(class class class)co 7377
Cℋ cch 29968
∨ℋ chj 29972 |
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 2702 ax-sep 5276 ax-nul 5283 ax-pr 5404 ax-hilex 30038 |
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-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3419 df-v 3461 df-sbc 3758 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-br 5126 df-opab 5188 df-id 5551 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-iota 6468 df-fun 6518 df-fv 6524 df-ov 7380 df-oprab 7381 df-mpo 7382 df-sh 30246 df-ch 30260 df-chj 30349 |
This theorem is referenced by: chub2i
30509 chnlei
30524 chj12i
30561 lejdiri
30578 cmcm2i
30632 cmbr3i
30639 qlax2i
30667 osumcor2i
30683 3oalem5
30705 pjcji
30723 mayetes3i
30768 mdslj2i
31359 mdsl1i
31360 cvmdi
31363 mdslmd2i
31369 mdexchi
31374 cvexchi
31408 atabsi
31440 mdsymlem1
31442 mdsymlem6
31447 mdsymlem8
31449 sumdmdlem2
31458 dmdbr5ati
31461 |