Colors of
variables: wff
setvar class |
Syntax hints: ⊤wtru 1542 Ⅎwnf 1785
Ⅎwnfc 2883
℩crio 7366 |
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 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 df-v 3476 df-in 3955 df-ss 3965 df-sn 4629 df-uni 4909 df-iota 6495 df-riota 7367 |
This theorem is referenced by: csbriota
7383 nfoi
9511 lble
12170 nosupbnd1
27441 noinfbnd1
27456 riotasvd
38129 riotasv2d
38130 riotasv2s
38131 cdleme26ee
39534 cdleme31sn1
39555 cdlemefs32sn1aw
39588 cdleme43fsv1snlem
39594 cdleme41sn3a
39607 cdleme32d
39618 cdleme32f
39620 cdleme40m
39641 cdleme40n
39642 cdlemk36
40087 cdlemk38
40089 cdlemkid
40110 cdlemk19x
40117 cdlemk11t
40120 |