Theorem 2sb5

Description: Equivalence for double substitution. (Contributed by NM, 3-Feb-2005)

	Ref	Expression
Assertion	2sb5	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sb5	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑧 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) )
2		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ ( 𝑦 = 𝑤 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝑧 ∧ ∃ 𝑦 ( 𝑦 = 𝑤 ∧ 𝜑 ) ) )
3		anass	⊢ ( ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) ↔ ( 𝑥 = 𝑧 ∧ ( 𝑦 = 𝑤 ∧ 𝜑 ) ) )
4	3	exbii	⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 = 𝑧 ∧ ( 𝑦 = 𝑤 ∧ 𝜑 ) ) )
5		sb5	⊢ ( [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝑤 ∧ 𝜑 ) )
6	5	anbi2i	⊢ ( ( 𝑥 = 𝑧 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( 𝑥 = 𝑧 ∧ ∃ 𝑦 ( 𝑦 = 𝑤 ∧ 𝜑 ) ) )
7	2 4 6	3bitr4ri	⊢ ( ( 𝑥 = 𝑧 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )
8	7	exbii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑧 ∧ [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )
9	1 8	bitri	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ∧ 𝜑 ) )