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 3493 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3493 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 482 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1934 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2822 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 631 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1925 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4908 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3669 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 380 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  Vcvv 3475   cuni 4907
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-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-uni 4908
This theorem is referenced by:  eluni2  4911  elunii  4912  uniss  4915  eluniab  4922  uniun  4933  uniin  4934  unissb  4942  unissbOLD  4943  dfiun2g  5032  dftr2  5266  unipw  5449  dmuni  5912  iotanul2  6510  fununi  6620  elunirn  7245  uniex2  7723  uniuni  7744  mpoxopxnop0  8195  fprresex  8290  wfrfunOLD  8314  wfrlem17OLD  8320  tfrlem7  8378  tfrlem9a  8381  inf2  9614  inf3lem2  9620  rankwflemb  9784  cardprclem  9970  carduni  9972  iunfictbso  10105  kmlem3  10143  kmlem4  10144  cfub  10240  isf34lem4  10368  grothtsk  10826  suplem1pr  11043  toprntopon  22409  isbasis2g  22433  tgval2  22441  ntreq0  22563  cmpsublem  22885  cmpsub  22886  cmpcld  22888  is1stc2  22928  alexsubALTlem3  23535  alexsubALT  23537  elold  27344  fnessref  35180  bj-restuni  35916  difunieq  36193  ismnushort  42993  truniALT  43235  truniALTVD  43572  unisnALT  43620  elunif  43633  ssfiunibd  43954  stoweidlem27  44678  stoweidlem48  44699  setrec1lem3  47636  setrec1  47638
  Copyright terms: Public domain W3C validator