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

Theorem eluniab 4923
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 4911 . 2 (𝐴 {𝑥𝜑} ↔ ∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}))
2 nfv 1918 . . . 4 𝑥 𝐴𝑦
3 nfsab1 2718 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
42, 3nfan 1903 . . 3 𝑥(𝐴𝑦𝑦 ∈ {𝑥𝜑})
5 nfv 1918 . . 3 𝑦(𝐴𝑥𝜑)
6 eleq2w 2818 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
7 eleq1w 2817 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2714 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8bitrdi 287 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
106, 9anbi12d 632 . . 3 (𝑦 = 𝑥 → ((𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ (𝐴𝑥𝜑)))
114, 5, 10cbvexv1 2339 . 2 (∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑥(𝐴𝑥𝜑))
121, 11bitri 275 1 (𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  {cab 2710   cuni 4908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-uni 4909
This theorem is referenced by:  elunirab  4924  dfiun2gOLD  5034  inuni  5343  elfv  6887  unielxp  8010  frrlem8  8275  frrlem10  8277  wfrlem12OLD  8317  tfrlem9  8382  dfac5lem2  10116  fin23lem30  10334  unisngl  23023  metrest  24025  aannenlem2  25834  fpwrelmapffslem  31945  dfiota3  34884  mptsnunlem  36208  nnoeomeqom  42048
  Copyright terms: Public domain W3C validator