Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Proper substitution of classes for sets
sbc2ie
Metamath Proof Explorer
Description: Conversion of implicit substitution to explicit class substitution.
(Contributed by NM , 16-Dec-2008) (Revised by Mario Carneiro , 19-Dec-2013)
Ref
Expression
Hypotheses
sbc2ie.1
⊢ A ∈ V
sbc2ie.2
⊢ B ∈ V
sbc2ie.3
⊢ x = A ∧ y = B → φ ↔ ψ
Assertion
sbc2ie
⊢ [ ˙ A / x ] ˙ [ ˙ B / y ] ˙ φ ↔ ψ
Proof
Step
Hyp
Ref
Expression
1
sbc2ie.1
⊢ A ∈ V
2
sbc2ie.2
⊢ B ∈ V
3
sbc2ie.3
⊢ x = A ∧ y = B → φ ↔ ψ
4
nfv
⊢ Ⅎ x ψ
5
nfv
⊢ Ⅎ y ψ
6
2
nfth
⊢ Ⅎ x B ∈ V
7
4 5 6 3
sbc2iegf
⊢ A ∈ V ∧ B ∈ V → [ ˙ A / x ] ˙ [ ˙ B / y ] ˙ φ ↔ ψ
8
1 2 7
mp2an
⊢ [ ˙ A / x ] ˙ [ ˙ B / y ] ˙ φ ↔ ψ