Theorem 2sb6rf

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 variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (Proof shortened by Wolf Lammen, 13-Apr-2023) (New usage is discouraged.)

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

Proof

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