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

Theorem eluniab 4438
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 4430 . 2 (𝐴 {𝑥𝜑} ↔ ∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}))
2 nfv 1841 . . . 4 𝑥 𝐴𝑦
3 nfsab1 2610 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
42, 3nfan 1826 . . 3 𝑥(𝐴𝑦𝑦 ∈ {𝑥𝜑})
5 nfv 1841 . . 3 𝑦(𝐴𝑥𝜑)
6 eleq2 2688 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
7 eleq1 2687 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2608 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 276 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
106, 9anbi12d 746 . . 3 (𝑦 = 𝑥 → ((𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ (𝐴𝑥𝜑)))
114, 5, 10cbvex 2270 . 2 (∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑥(𝐴𝑥𝜑))
121, 11bitri 264 1 (𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1702  wcel 1988  {cab 2606   cuni 4427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-uni 4428
This theorem is referenced by:  elunirab  4439  dfiun2g  4543  inuni  4817  elfv  6176  snnexOLD  6952  unielxp  7189  wfrlem12  7411  tfrlem9  7466  dfac5lem2  8932  fin23lem30  9149  unisngl  21311  metrest  22310  aannenlem2  24065  fpwrelmapffslem  29481  frrlem11  31766  dfiota3  32005  mptsnunlem  33156
  Copyright terms: Public domain W3C validator