Metamath Proof Explorer


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 ( 𝜑 ↔ ∃ 𝑧𝑤 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )