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 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  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  7671  uniuni  7692  mpoxopxnop0  8142  fprresex  8237  wfrfunOLD  8261  wfrlem17OLD  8267  tfrlem7  8325  tfrlem9a  8328  inf2  9555  inf3lem2  9561  rankwflemb  9725  cardprclem  9911  carduni  9913  iunfictbso  10046  kmlem3  10084  kmlem4  10085  cfub  10181  isf34lem4  10309  grothtsk  10767  suplem1pr  10984  toprntopon  22258  isbasis2g  22282  tgval2  22290  ntreq0  22412  cmpsublem  22734  cmpsub  22735  cmpcld  22737  is1stc2  22777  alexsubALTlem3  23384  alexsubALT  23386  elold  27183  fnessref  34796  bj-restuni  35535  difunieq  35812  ismnushort  42523  truniALT  42765  truniALTVD  43102  unisnALT  43150  elunif  43163  ssfiunibd  43479  stoweidlem27  44200  stoweidlem48  44221  setrec1lem3  47066  setrec1  47068
  Copyright terms: Public domain W3C validator