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 ( ( 𝐴𝑉 ∧ Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ) → ( [ 𝐴 / 𝑥 ] 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 sbc6g ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ) )
2 1 3ad2ant1 ( ( 𝐴𝑉 ∧ Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ) )
3 ceqsalt ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ 𝐴𝑉 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜓 ) )
4 3 3comr ( ( 𝐴𝑉 ∧ Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ) → ( ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜓 ) )
5 2 4 bitrd ( ( 𝐴𝑉 ∧ Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ) → ( [ 𝐴 / 𝑥 ] 𝜑𝜓 ) )