Colors of
variables: wff
setvar class |
Syntax hints: ⊤wtru 1543 Ⅎwnf 1786
Ⅎwnfc 2884
℩crio 7364 |
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 2704 |
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 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-v 3477 df-in 3956 df-ss 3966 df-sn 4630 df-uni 4910 df-iota 6496 df-riota 7365 |
This theorem is referenced by: csbriota
7381 nfoi
9509 lble
12166 nosupbnd1
27217 noinfbnd1
27232 riotasvd
37874 riotasv2d
37875 riotasv2s
37876 cdleme26ee
39279 cdleme31sn1
39300 cdlemefs32sn1aw
39333 cdleme43fsv1snlem
39339 cdleme41sn3a
39352 cdleme32d
39363 cdleme32f
39365 cdleme40m
39386 cdleme40n
39387 cdlemk36
39832 cdlemk38
39834 cdlemkid
39855 cdlemk19x
39862 cdlemk11t
39865 |