Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∈ wcel 2107
∅c0 4286 1oc1o 8409 |
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 ax-nul 5267 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3449 df-dif 3917 df-un 3919 df-nul 4287 df-sn 4591 df-suc 6327 df-1o 8416 |
This theorem is referenced by: dif20el
8455 oe1m
8496 oen0
8537 oeoa
8548 oeoe
8550 isfin4p1
10259 fin1a2lem4
10347 1lt2pi
10849 indpi
10851 sadcp1
16343 vr1cl2
21587 fvcoe1
21601 vr1cl
21611 subrgvr1cl
21656 coe1mul2lem1
21661 coe1tm
21667 ply1coe
21690 evl1var
21725 evls1var
21727 xkofvcn
23058 pw2f1ocnv
41408 wepwsolem
41416 onexoegt
41625 oaordnrex
41677 omnord1ex
41686 omcl3g
41716 indthinc
47162 indthincALT
47163 prsthinc
47164 |