Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eusv2nf Structured version   Visualization version   GIF version

Theorem eusv2nf 5283
 Description: Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by Mario Carneiro, 18-Nov-2016.)
Hypothesis
Ref Expression
eusv2.1 𝐴 ∈ V
Assertion
Ref Expression
eusv2nf (∃!𝑦𝑥 𝑦 = 𝐴𝑥𝐴)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem eusv2nf
StepHypRef Expression
1 nfeu1 2675 . . . 4 𝑦∃!𝑦𝑥 𝑦 = 𝐴
2 nfe1 2155 . . . . . . 7 𝑥𝑥 𝑦 = 𝐴
32nfeuw 2680 . . . . . 6 𝑥∃!𝑦𝑥 𝑦 = 𝐴
4 eusv2.1 . . . . . . . . 9 𝐴 ∈ V
54isseti 3494 . . . . . . . 8 𝑦 𝑦 = 𝐴
6 19.8a 2182 . . . . . . . . 9 (𝑦 = 𝐴 → ∃𝑥 𝑦 = 𝐴)
76ancri 553 . . . . . . . 8 (𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴𝑦 = 𝐴))
85, 7eximii 1838 . . . . . . 7 𝑦(∃𝑥 𝑦 = 𝐴𝑦 = 𝐴)
9 eupick 2721 . . . . . . 7 ((∃!𝑦𝑥 𝑦 = 𝐴 ∧ ∃𝑦(∃𝑥 𝑦 = 𝐴𝑦 = 𝐴)) → (∃𝑥 𝑦 = 𝐴𝑦 = 𝐴))
108, 9mpan2 690 . . . . . 6 (∃!𝑦𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴𝑦 = 𝐴))
113, 10alrimi 2215 . . . . 5 (∃!𝑦𝑥 𝑦 = 𝐴 → ∀𝑥(∃𝑥 𝑦 = 𝐴𝑦 = 𝐴))
12 nf6 2293 . . . . 5 (Ⅎ𝑥 𝑦 = 𝐴 ↔ ∀𝑥(∃𝑥 𝑦 = 𝐴𝑦 = 𝐴))
1311, 12sylibr 237 . . . 4 (∃!𝑦𝑥 𝑦 = 𝐴 → Ⅎ𝑥 𝑦 = 𝐴)
141, 13alrimi 2215 . . 3 (∃!𝑦𝑥 𝑦 = 𝐴 → ∀𝑦𝑥 𝑦 = 𝐴)
15 dfnfc2 4846 . . . 4 (∀𝑥 𝐴 ∈ V → (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦 = 𝐴))
1615, 4mpg 1799 . . 3 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦 = 𝐴)
1714, 16sylibr 237 . 2 (∃!𝑦𝑥 𝑦 = 𝐴𝑥𝐴)
18 eusvnfb 5281 . . . 4 (∃!𝑦𝑥 𝑦 = 𝐴 ↔ (𝑥𝐴𝐴 ∈ V))
194, 18mpbiran2 709 . . 3 (∃!𝑦𝑥 𝑦 = 𝐴𝑥𝐴)
20 eusv2i 5282 . . 3 (∃!𝑦𝑥 𝑦 = 𝐴 → ∃!𝑦𝑥 𝑦 = 𝐴)
2119, 20sylbir 238 . 2 (𝑥𝐴 → ∃!𝑦𝑥 𝑦 = 𝐴)
2217, 21impbii 212 1 (∃!𝑦𝑥 𝑦 = 𝐴𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2115  ∃!weu 2654  Ⅎwnfc 2962  Vcvv 3480 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-sn 4551  df-pr 4553  df-uni 4825 This theorem is referenced by:  eusv2  5284
 Copyright terms: Public domain W3C validator