Theorem 2sb5rf

Description: Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Feb-2005) (Revised by Mario Carneiro, 6-Oct-2016) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2sb5rf.1	⊢ Ⅎ 𝑧 𝜑
	2sb5rf.2	⊢ Ⅎ 𝑤 𝜑
Assertion	2sb5rf	⊢ ( 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		2sb5rf.1	⊢ Ⅎ 𝑧 𝜑
2		2sb5rf.2	⊢ Ⅎ 𝑤 𝜑
3	1	19.41	⊢ ( ∃ 𝑧 ( ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
4	2	19.41	⊢ ( ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
5	4	exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ( ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
6		2ax6e	⊢ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 )
7	6	biantrur	⊢ ( 𝜑 ↔ ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
8	3 5 7	3bitr4ri	⊢ ( 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
9		sbequ12r	⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 ) )
10		sbequ12r	⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
11	9 10	sylan9bb	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
12	11	pm5.32i	⊢ ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
13	12	2exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
14	8 13	bitr4i	⊢ ( 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )