This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Proper substitution of classes for sets into classes csbieb
Description: Bidirectional conversion between an implicit class substitution
hypothesis x = A -> B = C and its explicit substitution equivalent.
(Contributed by NM , 2-Mar-2008)
Ref
Expression
Hypotheses
csbieb.1 ⊢ 𝐴 ∈ V
csbieb.2 ⊢ Ⅎ 𝑥 𝐶
Assertion
csbieb ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )
Proof
Step
Hyp
Ref
Expression
1
csbieb.1 ⊢ 𝐴 ∈ V
2
csbieb.2 ⊢ Ⅎ 𝑥 𝐶
3
csbiebt ⊢ ( ( 𝐴 ∈ V ∧ Ⅎ 𝑥 𝐶 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
4
1 2 3
mp2an ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )