Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
scotteqd
Next ⟩
scotteq
Metamath Proof Explorer
Ascii
Unicode
Theorem
scotteqd
Description:
Equality theorem for the Scott operation.
(Contributed by
Rohan Ridenour
, 9-Aug-2023)
Ref
Expression
Hypothesis
scotteqd.1
⊢
φ
→
A
=
B
Assertion
scotteqd
⊢
φ
→
Scott
A
=
Scott
B
Proof
Step
Hyp
Ref
Expression
1
scotteqd.1
⊢
φ
→
A
=
B
2
1
adantr
⊢
φ
∧
x
∈
A
→
A
=
B
3
2
raleqdv
⊢
φ
∧
x
∈
A
→
∀
y
∈
A
rank
⁡
x
⊆
rank
⁡
y
↔
∀
y
∈
B
rank
⁡
x
⊆
rank
⁡
y
4
1
3
rabeqbidva
⊢
φ
→
x
∈
A
|
∀
y
∈
A
rank
⁡
x
⊆
rank
⁡
y
=
x
∈
B
|
∀
y
∈
B
rank
⁡
x
⊆
rank
⁡
y
5
df-scott
⊢
Scott
A
=
x
∈
A
|
∀
y
∈
A
rank
⁡
x
⊆
rank
⁡
y
6
df-scott
⊢
Scott
B
=
x
∈
B
|
∀
y
∈
B
rank
⁡
x
⊆
rank
⁡
y
7
4
5
6
3eqtr4g
⊢
φ
→
Scott
A
=
Scott
B