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

Metamath Proof Explorer

Theorem bnj610

Description: Pass from equality ( x = A ) to substitution ( [. A / x ]. ) without the distinct variable condition on A , x . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj610.1 ⊢ 𝐴 ∈ V
bnj610.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
bnj610.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓′ ) )
bnj610.4 ⊢ ( 𝑦 = 𝐴 → ( 𝜓′ ↔ 𝜓 ) )
Assertion bnj610 ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 bnj610.1 ⊢ 𝐴 ∈ V
2 bnj610.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 bnj610.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓′ ) )
4 bnj610.4 ⊢ ( 𝑦 = 𝐴 → ( 𝜓′ ↔ 𝜓 ) )
5 vex ⊢ 𝑦 ∈ V
6 5 3 sbcie ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓′ )
7 6 sbcbii ⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] 𝜓′ )
8 sbccow ⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 )
9 1 4 sbcie ⊢ ( [ 𝐴 / 𝑦 ] 𝜓′ ↔ 𝜓 )
10 7 8 9 3bitr3i ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )