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

Theorem eluniab 4591
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 4583 . 2 (𝐴 {𝑥𝜑} ↔ ∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}))
2 nfv 1984 . . . 4 𝑥 𝐴𝑦
3 nfsab1 2742 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
42, 3nfan 1969 . . 3 𝑥(𝐴𝑦𝑦 ∈ {𝑥𝜑})
5 nfv 1984 . . 3 𝑦(𝐴𝑥𝜑)
6 eleq2w 2815 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
7 eleq1w 2814 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2740 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 276 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
106, 9anbi12d 749 . . 3 (𝑦 = 𝑥 → ((𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ (𝐴𝑥𝜑)))
114, 5, 10cbvex 2409 . 2 (∃𝑦(𝐴𝑦𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑥(𝐴𝑥𝜑))
121, 11bitri 264 1 (𝐴 {𝑥𝜑} ↔ ∃𝑥(𝐴𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1845  wcel 2131  {cab 2738   cuni 4580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-uni 4581
This theorem is referenced by:  elunirab  4592  dfiun2g  4696  inuni  4967  elfv  6342  snnexOLD  7124  unielxp  7363  wfrlem12  7587  tfrlem9  7642  dfac5lem2  9129  fin23lem30  9348  unisngl  21524  metrest  22522  aannenlem2  24275  fpwrelmapffslem  29808  frrlem11  32090  dfiota3  32328  mptsnunlem  33488
  Copyright terms: Public domain W3C validator