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

Theorem eluni 4866
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 3461 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3461 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 481 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1933 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2825 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 630 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1924 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4864 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3630 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 379 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  Vcvv 3443   cuni 4863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-uni 4864
This theorem is referenced by:  eluni2  4867  elunii  4868  uniss  4871  eluniab  4878  uniun  4889  uniin  4890  unissb  4898  unissbOLD  4899  dfiun2g  4988  dftr2  5222  unipw  5405  dmuni  5868  iotanul2  6463  fununi  6573  elunirn  7194  uniex2  7667  uniuni  7688  mpoxopxnop0  8138  fprresex  8233  wfrfunOLD  8257  wfrlem17OLD  8263  tfrlem7  8321  tfrlem9a  8324  inf2  9517  inf3lem2  9523  rankwflemb  9687  cardprclem  9873  carduni  9875  iunfictbso  10008  kmlem3  10046  kmlem4  10047  cfub  10143  isf34lem4  10271  grothtsk  10729  suplem1pr  10946  toprntopon  22226  isbasis2g  22250  tgval2  22258  ntreq0  22380  cmpsublem  22702  cmpsub  22703  cmpcld  22705  is1stc2  22745  alexsubALTlem3  23352  alexsubALT  23354  elold  27151  fnessref  34767  bj-restuni  35506  difunieq  35783  ismnushort  42492  truniALT  42734  truniALTVD  43071  unisnALT  43119  elunif  43132  ssfiunibd  43448  stoweidlem27  44169  stoweidlem48  44190  setrec1lem3  47035  setrec1  47037
  Copyright terms: Public domain W3C validator