Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 ∈ wcel 2099
∀wral 3058 ⊆
wss 3947 Tr wtr 5265 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-ext 2699 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-v 3473 df-in 3954 df-ss 3964 df-uni 4909 df-tr 5266 |
This theorem is referenced by: trss
5276 trin
5277 triun
5280 triin
5282 tron
6392 ssorduni
7781 sucexeloniOLD
7813 suceloniOLD
7815 dfrecs3
8392 dfrecs3OLD
8393 ordtypelem2
9542 tcwf
9906 itunitc
10444 wunex2
10761 wfgru
10839 nadd2rabtr
42813 |