Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 ∩ cin 3948 |
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-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 |
This theorem is referenced by: isfin1-3
10381 setc2ohom
18045 isdrs2
18259 fpwipodrs
18493 0cmp
22898 comppfsc
23036 ptcmpfi
23317 alexsubALTlem2
23552 alexsubALTlem4
23554 ptcmp
23562 cnstrcvs
24657 cncvs
24661 recvs
24662 recvsOLD
24663 qcvs
24664 cnncvs
24676 ovolicc1
25033 ioorf
25090 corclrcl
42458 0pwfi
43746 sge0rnn0
45084 sge0reuz
45163 |