Colors of
variables: wff
setvar class |
Syntax hints: ⊤wtru 1543 Ⅎwnf 1786
Ⅎwnfc 2888
℩crio 7313 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ral 3066 df-rex 3075 df-v 3448 df-in 3918 df-ss 3928 df-sn 4588 df-uni 4867 df-iota 6449 df-riota 7314 |
This theorem is referenced by: csbriota
7330 nfoi
9451 lble
12108 nosupbnd1
27065 noinfbnd1
27080 riotasvd
37421 riotasv2d
37422 riotasv2s
37423 cdleme26ee
38826 cdleme31sn1
38847 cdlemefs32sn1aw
38880 cdleme43fsv1snlem
38886 cdleme41sn3a
38899 cdleme32d
38910 cdleme32f
38912 cdleme40m
38933 cdleme40n
38934 cdlemk36
39379 cdlemk38
39381 cdlemkid
39402 cdlemk19x
39409 cdlemk11t
39412 |