Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 ∈ wcel 2107
Vcvv 3475 ∪ cuni 4909 |
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-sep 5300 ax-pow 5364 ax-un 7725 |
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-rab 3434 df-v 3477 df-in 3956 df-ss 3966 df-pw 4605 df-uni 4910 |
This theorem is referenced by: elpwpwel
7754 ixpexg
8916 rankuni
9858 unialeph
10096 ttukeylem1
10504 tgss2
22490 ordtbas2
22695 ordtbas
22696 ordttopon
22697 ordtopn1
22698 ordtopn2
22699 ordtrest2
22708 isref
23013 islocfin
23021 txbasex
23070 ptbasin2
23082 ordthmeolem
23305 alexsublem
23548 alexsub
23549 alexsubb
23550 ussid
23765 ordtrest2NEW
32903 brbigcup
34870 isfne
35224 isfne4
35225 isfne4b
35226 fnessref
35242 neibastop1
35244 fnejoin2
35254 prtex
37750 |