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

Theorem eluni 4914
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 3498 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3498 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 480 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1927 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2826 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 631 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1918 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4912 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3682 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 378 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1536  wex 1775  wcel 2105  Vcvv 3477   cuni 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-uni 4912
This theorem is referenced by:  eluni2  4915  elunii  4916  uniss  4919  eluniab  4925  uniun  4934  uniin  4935  unissb  4943  unissbOLD  4944  dfiun2g  5034  dftr2  5266  unipw  5460  dmuni  5927  iotanul2  6532  fununi  6642  elunirn  7270  uniex2  7756  uniuni  7780  mpoxopxnop0  8238  fprresex  8333  wfrfunOLD  8357  wfrlem17OLD  8363  tfrlem7  8421  tfrlem9a  8424  inf2  9660  inf3lem2  9666  rankwflemb  9830  cardprclem  10016  carduni  10018  iunfictbso  10151  kmlem3  10190  kmlem4  10191  cfub  10286  isf34lem4  10414  grothtsk  10872  suplem1pr  11089  toprntopon  22946  isbasis2g  22970  tgval2  22978  ntreq0  23100  cmpsublem  23422  cmpsub  23423  cmpcld  23425  is1stc2  23465  alexsubALTlem3  24072  alexsubALT  24074  elold  27922  fnessref  36339  bj-restuni  37079  difunieq  37356  ismnushort  44296  truniALT  44538  truniALTVD  44875  unisnALT  44923  elunif  44953  ssfiunibd  45259  stoweidlem27  45982  stoweidlem48  46003  setrec1lem3  48919  setrec1  48921
  Copyright terms: Public domain W3C validator