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

Theorem eluni 4910
Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eluni
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elex 3501 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3501 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 480 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1930 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2829 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 631 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1921 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4908 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3680 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 378 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  Vcvv 3480   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-uni 4908
This theorem is referenced by:  eluni2  4911  elunii  4912  uniss  4915  eluniab  4921  uniun  4930  uniin  4931  unissb  4939  unissbOLD  4940  dfiun2g  5030  dftr2  5261  unipw  5455  dmuni  5925  iotanul2  6531  fununi  6641  elunirn  7271  uniex2  7758  uniuni  7782  mpoxopxnop0  8240  fprresex  8335  wfrfunOLD  8359  wfrlem17OLD  8365  tfrlem7  8423  tfrlem9a  8426  inf2  9663  inf3lem2  9669  rankwflemb  9833  cardprclem  10019  carduni  10021  iunfictbso  10154  kmlem3  10193  kmlem4  10194  cfub  10289  isf34lem4  10417  grothtsk  10875  suplem1pr  11092  toprntopon  22931  isbasis2g  22955  tgval2  22963  ntreq0  23085  cmpsublem  23407  cmpsub  23408  cmpcld  23410  is1stc2  23450  alexsubALTlem3  24057  alexsubALT  24059  elold  27908  fnessref  36358  bj-restuni  37098  difunieq  37375  ismnushort  44320  truniALT  44561  truniALTVD  44898  unisnALT  44946  uniclaxun  45003  elunif  45021  ssfiunibd  45321  stoweidlem27  46042  stoweidlem48  46063  setrec1lem3  49208  setrec1  49210
  Copyright terms: Public domain W3C validator