Theorem a12stdy1 1370

Description: Part of a study related to ax-12 966. The consequent introduces a new variable z. There are no distinct variable restrictions.

Assertion

Ref	Expression
a12stdy1	⊢ (∀x x = y → ∃x y = z)

Proof of Theorem a12stdy1

Step	Hyp	Ref	Expression
1		a9e 1123	. 2 ⊢ ∃y y = z
2		ax-10o 1138	. . . 4 ⊢ (∀x x = y → (∀x ¬ y = z → ∀y ¬ y = z))
3	2	con3d 95	. . 3 ⊢ (∀x x = y → (¬ ∀y ¬ y = z → ¬ ∀x ¬ y = z))
4		df-ex 979	. . 3 ⊢ (∃y y = z ↔ ¬ ∀y ¬ y = z)
5		df-ex 979	. . 3 ⊢ (∃x y = z ↔ ¬ ∀x ¬ y = z)
6	3, 4, 5	3imtr4g 552	. 2 ⊢ (∀x x = y → (∃y y = z → ∃x y = z))
7	1, 6	mpi 44	1 ⊢ (∀x x = y → ∃x y = z)

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 952   = wceq 954  ∃wex 978

This theorem is referenced by:  a12stdy3 1372

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-9 963  ax-10o 1138

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979

Copyright terms: Public domain