Theorem dveeq2or 1694

Description: Quantifier introduction when one pair of variables is distinct. Like dveeq2 1693 but connecting ∀xx = y by a disjunction rather than negation and implication makes the theorem stronger in intuitionistic logic. (Contributed by Jim Kingdon, 1-Feb-2018.)

Assertion

Ref	Expression
dveeq2or	⊢ (∀x x = y ∨ Ⅎx z = y)

Distinct variable group:   x,z

Proof of Theorem dveeq2or

Step	Hyp	Ref	Expression
1		ax-i12 1395	. . . . . 6 ⊢ (∀x x = z ∨ (∀x x = y ∨ ∀x(z = y → ∀x z = y)))
2		orass 683	. . . . . 6 ⊢ (((∀x x = z ∨ ∀x x = y) ∨ ∀x(z = y → ∀x z = y)) ↔ (∀x x = z ∨ (∀x x = y ∨ ∀x(z = y → ∀x z = y))))
3	1, 2	mpbir 134	. . . . 5 ⊢ ((∀x x = z ∨ ∀x x = y) ∨ ∀x(z = y → ∀x z = y))
4		pm1.4 645	. . . . . 6 ⊢ ((∀x x = z ∨ ∀x x = y) → (∀x x = y ∨ ∀x x = z))
5	4	orim1i 676	. . . . 5 ⊢ (((∀x x = z ∨ ∀x x = y) ∨ ∀x(z = y → ∀x z = y)) → ((∀x x = y ∨ ∀x x = z) ∨ ∀x(z = y → ∀x z = y)))
6	3, 5	ax-mp 7	. . . 4 ⊢ ((∀x x = y ∨ ∀x x = z) ∨ ∀x(z = y → ∀x z = y))
7		orass 683	. . . 4 ⊢ (((∀x x = y ∨ ∀x x = z) ∨ ∀x(z = y → ∀x z = y)) ↔ (∀x x = y ∨ (∀x x = z ∨ ∀x(z = y → ∀x z = y))))
8	6, 7	mpbi 133	. . 3 ⊢ (∀x x = y ∨ (∀x x = z ∨ ∀x(z = y → ∀x z = y)))
9		ax16 1691	. . . . . 6 ⊢ (∀x x = z → (z = y → ∀x z = y))
10	9	a5i 1432	. . . . 5 ⊢ (∀x x = z → ∀x(z = y → ∀x z = y))
11		id 19	. . . . 5 ⊢ (∀x(z = y → ∀x z = y) → ∀x(z = y → ∀x z = y))
12	10, 11	jaoi 635	. . . 4 ⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) → ∀x(z = y → ∀x z = y))
13	12	orim2i 677	. . 3 ⊢ ((∀x x = y ∨ (∀x x = z ∨ ∀x(z = y → ∀x z = y))) → (∀x x = y ∨ ∀x(z = y → ∀x z = y)))
14	8, 13	ax-mp 7	. 2 ⊢ (∀x x = y ∨ ∀x(z = y → ∀x z = y))
15		df-nf 1347	. . . 4 ⊢ (Ⅎx z = y ↔ ∀x(z = y → ∀x z = y))
16	15	biimpri 124	. . 3 ⊢ (∀x(z = y → ∀x z = y) → Ⅎx z = y)
17	16	orim2i 677	. 2 ⊢ ((∀x x = y ∨ ∀x(z = y → ∀x z = y)) → (∀x x = y ∨ Ⅎx z = y))
18	14, 17	ax-mp 7	1 ⊢ (∀x x = y ∨ Ⅎx z = y)

Syntax hints:   → wi 4   ∨ wo 628  ∀wal 1240  Ⅎwnf 1346

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643

This theorem is referenced by:  equs5or  1708  sbal1yz  1874  copsexg  3972