Theorem bnj610

Description: Pass from equality ( x = A ) to substitution ( [. A / x ]. ) without the distinct variable restriction ($d 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	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )