Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
scottex2
Next ⟩
scotteld
Metamath Proof Explorer
Ascii
Unicode
Theorem
scottex2
Description:
scottex
expressed using
Scott
.
(Contributed by
Rohan Ridenour
, 9-Aug-2023)
Ref
Expression
Assertion
scottex2
⊢
Scott
A
∈
V
Proof
Step
Hyp
Ref
Expression
1
df-scott
⊢
Scott
A
=
x
∈
A
|
∀
y
∈
A
rank
⁡
x
⊆
rank
⁡
y
2
scottex
⊢
x
∈
A
|
∀
y
∈
A
rank
⁡
x
⊆
rank
⁡
y
∈
V
3
1
2
eqeltri
⊢
Scott
A
∈
V