Theorem drsb1

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jun-1993) (New usage is discouraged.)

	Ref	Expression
Assertion	drsb1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		equequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
2	1	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
3	2	imbi1d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑧 → 𝜑 ) ↔ ( 𝑦 = 𝑧 → 𝜑 ) ) )
4	2	anbi1d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑧 ∧ 𝜑 ) ↔ ( 𝑦 = 𝑧 ∧ 𝜑 ) ) )
5	4	drex1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 = 𝑧 ∧ 𝜑 ) ) )
6	3 5	anbi12d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( ( 𝑥 = 𝑧 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝜑 ) ) ↔ ( ( 𝑦 = 𝑧 → 𝜑 ) ∧ ∃ 𝑦 ( 𝑦 = 𝑧 ∧ 𝜑 ) ) ) )
7		dfsb1	⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑧 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝜑 ) ) )
8		dfsb1	⊢ ( [ 𝑧 / 𝑦 ] 𝜑 ↔ ( ( 𝑦 = 𝑧 → 𝜑 ) ∧ ∃ 𝑦 ( 𝑦 = 𝑧 ∧ 𝜑 ) ) )
9	6 7 8	3bitr4g	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )