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

Theorem eluniab 4851
Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
Assertion
Ref Expression
eluniab (𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eluniab
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eluni 4839 . 2 (𝐴 {𝑥𝜑} ↔ ∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}))
2 nfv 1918 . . . 4 𝑥 𝐴𝑦
3 nfsab1 2723 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
42, 3nfan 1903 . . 3 𝑥(𝐴𝑦𝑦 ∈ {𝑥𝜑})
5 nfv 1918 . . 3 𝑦(𝐴𝑥𝜑)
6 eleq2w 2822 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
7 eleq1w 2821 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2719 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8bitrdi 286 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
106, 9anbi12d 630 . . 3 (𝑦 = 𝑥 → ((𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ (𝐴𝑥𝜑)))
114, 5, 10cbvexv1 2341 . 2 (∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑥(𝐴𝑥𝜑))
121, 11bitri 274 1 (𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395  wex 1783  wcel 2108  {cab 2715   cuni 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-uni 4837
This theorem is referenced by:  elunirab  4852  dfiun2g  4957  inuni  5262  elfv  6754  unielxp  7842  frrlem8  8080  frrlem10  8082  wfrlem12OLD  8122  tfrlem9  8187  dfac5lem2  9811  fin23lem30  10029  unisngl  22586  metrest  23586  aannenlem2  25394  fpwrelmapffslem  30969  dfiota3  34152  mptsnunlem  35436
  Copyright terms: Public domain W3C validator