This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2sb5nd

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2sb5nd ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 ax6e2ndeq ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
2 anabs5 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
3 2pm13.193 ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
4 3 exbii ⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
5 nfs1v ⊢ Ⅎ 𝑦 [ 𝑣 / 𝑦 ] 𝜑
6 5 nfsb ⊢ Ⅎ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑
7 6 19.41 ⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
8 4 7 bitr3i ⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
9 8 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
10 nfs1v ⊢ Ⅎ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑
11 10 19.41 ⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
12 9 11 bitr2i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
13 12 anbi2i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
14 2 13 bitr3i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
15 pm5.32 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) ) )
16 14 15 mpbir ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
17 1 16 sylbi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )