Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Scott's trick; collection principle; Hilbert's epsilon
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