Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 394
∧ w3a 1084 ∈
wcel 2098 ∀wral 3058
Vcvv 3473 ⊆ wss 3949
class class class wbr 5152
No csur 27593 <s cslt 27594
<<s csslt 27733 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pr 5433 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-br 5153 df-opab 5215 df-xp 5688 df-sslt 27734 |
This theorem is referenced by: sssslt1
27748 sssslt2
27749 conway
27752 sslttr
27760 ssltun1
27761 ssltun2
27762 etasslt
27766 slerec
27772 sltrec
27773 cofsslt
27858 coinitsslt
27859 cofcut1
27860 cofcutr
27864 cutlt
27872 addsuniflem
27938 negsunif
27987 ssltmul1
28067 ssltmul2
28068 mulsuniflem
28069 mulsunif2lem
28089 precsexlem11
28135 renegscl
28246 |