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

Theorem eluniab 4605
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 4597 . 2 (𝐴 {𝑥𝜑} ↔ ∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}))
2 nfv 2009 . . . 4 𝑥 𝐴𝑦
3 nfsab1 2755 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
42, 3nfan 1998 . . 3 𝑥(𝐴𝑦𝑦 ∈ {𝑥𝜑})
5 nfv 2009 . . 3 𝑦(𝐴𝑥𝜑)
6 eleq2w 2828 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
7 eleq1w 2827 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2753 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 278 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
106, 9anbi12d 624 . . 3 (𝑦 = 𝑥 → ((𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ (𝐴𝑥𝜑)))
114, 5, 10cbvex 2377 . 2 (∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑥(𝐴𝑥𝜑))
121, 11bitri 266 1 (𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wex 1874  wcel 2155  {cab 2751   cuni 4594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-uni 4595
This theorem is referenced by:  elunirab  4606  dfiun2g  4708  inuni  4984  elfv  6373  snnexOLD  7165  unielxp  7404  wfrlem12  7630  tfrlem9  7685  dfac5lem2  9198  fin23lem30  9417  unisngl  21610  metrest  22608  aannenlem2  24375  fpwrelmapffslem  29891  frrlem11  32168  dfiota3  32406  mptsnunlem  33551
  Copyright terms: Public domain W3C validator