This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcie2g

Description: Conversion of implicit substitution to explicit class substitution. This version of sbcie avoids a disjointness condition on x , A by substituting twice. (Contributed by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses sbcie2g.1 ⊢ x = y → φ ↔ ψ
sbcie2g.2 ⊢ y = A → ψ ↔ χ
Assertion sbcie2g ⊢ A ∈ V → [˙A / x]˙ φ ↔ χ

Proof

Step Hyp Ref Expression
1 sbcie2g.1 ⊢ x = y → φ ↔ ψ
2 sbcie2g.2 ⊢ y = A → ψ ↔ χ
3 dfsbcq ⊢ y = A → [˙y / x]˙ φ ↔ [˙A / x]˙ φ
4 sbsbc ⊢ y x φ ↔ [˙y / x]˙ φ
5 1 sbievw ⊢ y x φ ↔ ψ
6 4 5 bitr3i ⊢ [˙y / x]˙ φ ↔ ψ
7 3 2 6 vtoclbg ⊢ A ∈ V → [˙A / x]˙ φ ↔ χ