Metamath Proof Explorer

Theorem sbciegft

Description: Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf .) (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016) (Proof shortened by SN, 14-May-2025)

Ref Expression
Assertion sbciegft ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbc6g ⊢ A ∈ V → [˙A / x]˙ φ ↔ ∀ x x = A → φ
2 1 3ad2ant1 ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ∀ x x = A → φ
3 ceqsalt ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ ↔ ψ
4 3 3comr ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ∀ x x = A → φ ↔ ψ
5 2 4 bitrd ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ψ