Theorem eusv2i 5368

Description: Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.)

Assertion

Ref	Expression
eusv2i	⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem eusv2i

Step	Hyp	Ref	Expression
1		nfeu1 2623	. . 3 ⊢ Ⅎ𝑦∃!𝑦∀𝑥 𝑦 = 𝐴
2		nfcvd 2932	. . . . . 6 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝑦)
3		eusvnf 5366	. . . . . 6 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴)
4	2, 3	nfeqd 2941	. . . . 5 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → Ⅎ𝑥 𝑦 = 𝐴)
5	4	nfrd 1818	. . . 4 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 → ∀𝑥 𝑦 = 𝐴))
6		19.2 2003	. . . 4 ⊢ (∀𝑥 𝑦 = 𝐴 → ∃𝑥 𝑦 = 𝐴)
7	5, 6	impbid1 228	. . 3 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 ↔ ∀𝑥 𝑦 = 𝐴))
8	1, 7	eubid 2621	. 2 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ ∃!𝑦∀𝑥 𝑦 = 𝐴))
9	8	ibir 271	1 ⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴)

Syntax hints:   → wi 4  ∀wal 1565   = wceq 1567  ∃wex 1806  ∃!weu 2602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-nul 4295

This theorem is referenced by:  eusv2nf  5369