Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
scotteq
Next ⟩
nfscott
Metamath Proof Explorer
Ascii
Unicode
Theorem
scotteq
Description:
Closed form of
scotteqd
.
(Contributed by
Rohan Ridenour
, 9-Aug-2023)
Ref
Expression
Assertion
scotteq
⊢
A
=
B
→
Scott
A
=
Scott
B
Proof
Step
Hyp
Ref
Expression
1
id
⊢
A
=
B
→
A
=
B
2
1
scotteqd
⊢
A
=
B
→
Scott
A
=
Scott
B