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

Theorem eluni 4912
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 4910 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3671 . 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 4909
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 4910
This theorem is referenced by:  eluni2  4913  elunii  4914  uniss  4917  eluniab  4924  uniun  4935  uniin  4936  unissb  4944  unissbOLD  4945  dfiun2g  5034  dftr2  5268  unipw  5451  dmuni  5915  iotanul2  6514  fununi  6624  elunirn  7250  uniex2  7728  uniuni  7749  mpoxopxnop0  8200  fprresex  8295  wfrfunOLD  8319  wfrlem17OLD  8325  tfrlem7  8383  tfrlem9a  8386  inf2  9618  inf3lem2  9624  rankwflemb  9788  cardprclem  9974  carduni  9976  iunfictbso  10109  kmlem3  10147  kmlem4  10148  cfub  10244  isf34lem4  10372  grothtsk  10830  suplem1pr  11047  toprntopon  22427  isbasis2g  22451  tgval2  22459  ntreq0  22581  cmpsublem  22903  cmpsub  22904  cmpcld  22906  is1stc2  22946  alexsubALTlem3  23553  alexsubALT  23555  elold  27364  fnessref  35242  bj-restuni  35978  difunieq  36255  ismnushort  43060  truniALT  43302  truniALTVD  43639  unisnALT  43687  elunif  43700  ssfiunibd  44019  stoweidlem27  44743  stoweidlem48  44764  setrec1lem3  47734  setrec1  47736
  Copyright terms: Public domain W3C validator