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

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