Theorem mor 1939

Description: Converse of mo23 1938 with an additional ∃xφ condition. (Contributed by Jim Kingdon, 25-Jun-2018.)

Hypothesis

Ref	Expression
mor.1	⊢ Ⅎyφ

Assertion

Ref	Expression
mor	⊢ (∃xφ → (∀x∀y((φ ∧ [y / x]φ) → x = y) → ∃y∀x(φ → x = y)))

Distinct variable group:   x,y

Allowed substitution hints:   φ(x,y)

Proof of Theorem mor

Step	Hyp	Ref	Expression
1		mor.1	. . 3 ⊢ Ⅎyφ
2	1	sb8e 1734	. 2 ⊢ (∃xφ ↔ ∃y[y / x]φ)
3		impexp 250	. . . . 5 ⊢ (((φ ∧ [y / x]φ) → x = y) ↔ (φ → ([y / x]φ → x = y)))
4		bi2.04 237	. . . . 5 ⊢ ((φ → ([y / x]φ → x = y)) ↔ ([y / x]φ → (φ → x = y)))
5	3, 4	bitri 173	. . . 4 ⊢ (((φ ∧ [y / x]φ) → x = y) ↔ ([y / x]φ → (φ → x = y)))
6	5	2albii 1357	. . 3 ⊢ (∀x∀y((φ ∧ [y / x]φ) → x = y) ↔ ∀x∀y([y / x]φ → (φ → x = y)))
7		nfs1v 1812	. . . . . 6 ⊢ Ⅎx[y / x]φ
8	7	nfri 1409	. . . . 5 ⊢ ([y / x]φ → ∀x[y / x]φ)
9	8	eximi 1488	. . . 4 ⊢ (∃y[y / x]φ → ∃y∀x[y / x]φ)
10		alim 1343	. . . . . . 7 ⊢ (∀x([y / x]φ → (φ → x = y)) → (∀x[y / x]φ → ∀x(φ → x = y)))
11	10	alimi 1341	. . . . . 6 ⊢ (∀y∀x([y / x]φ → (φ → x = y)) → ∀y(∀x[y / x]φ → ∀x(φ → x = y)))
12	11	a7s 1340	. . . . 5 ⊢ (∀x∀y([y / x]φ → (φ → x = y)) → ∀y(∀x[y / x]φ → ∀x(φ → x = y)))
13		exim 1487	. . . . 5 ⊢ (∀y(∀x[y / x]φ → ∀x(φ → x = y)) → (∃y∀x[y / x]φ → ∃y∀x(φ → x = y)))
14	12, 13	syl 14	. . . 4 ⊢ (∀x∀y([y / x]φ → (φ → x = y)) → (∃y∀x[y / x]φ → ∃y∀x(φ → x = y)))
15	9, 14	syl5com 26	. . 3 ⊢ (∃y[y / x]φ → (∀x∀y([y / x]φ → (φ → x = y)) → ∃y∀x(φ → x = y)))
16	6, 15	syl5bi 141	. 2 ⊢ (∃y[y / x]φ → (∀x∀y((φ ∧ [y / x]φ) → x = y) → ∃y∀x(φ → x = y)))
17	2, 16	sylbi 114	1 ⊢ (∃xφ → (∀x∀y((φ ∧ [y / x]φ) → x = y) → ∃y∀x(φ → x = y)))

Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1240  Ⅎwnf 1346  ∃wex 1378  [wsb 1642

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-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  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:  modc  1940