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]˙ φ ψ