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

Metamath Proof Explorer

Theorem ax6e2eq

Description: Alternate form of ax6e for non-distinct x , y and u = v . ax6e2eq is derived from ax6e2eqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2eq ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 ax6ev ⊢ ∃ 𝑥 𝑥 = 𝑢
2 hbae ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 )
3 ax7 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → 𝑦 = 𝑢 ) )
4 3 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → 𝑦 = 𝑢 ) )
5 4 ancld ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
6 2 5 eximdh ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝑥 = 𝑢 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
7 1 6 mpi ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
8 7 axc4i ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
9 axc11 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
10 8 9 mpd ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
11 19.2 ⊢ ( ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
12 10 11 syl ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
13 excomim ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
14 12 13 syl ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
15 equtrr ⊢ ( 𝑢 = 𝑣 → ( 𝑦 = 𝑢 → 𝑦 = 𝑣 ) )
16 15 anim2d ⊢ ( 𝑢 = 𝑣 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
17 16 2eximdv ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
18 14 17 syl5com ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )