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

Theorem eluni 4597
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 3365 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3365 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 472 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 2025 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2832 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 623 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 2016 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4595 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3508 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 369 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  Vcvv 3350   cuni 4594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-uni 4595
This theorem is referenced by:  eluni2  4598  elunii  4599  eluniab  4605  uniun  4615  uniin  4616  uniss  4617  unissb  4627  dftr2  4913  unipw  5074  dmuni  5502  fununi  6142  elunirn  6701  uniex2  7150  uniuni  7169  mpt2xopxnop0  7544  wfrfun  7629  wfrlem17  7635  tfrlem7  7683  tfrlem9a  7686  inf2  8735  inf3lem2  8741  rankwflemb  8871  cardprclem  9056  carduni  9058  iunfictbso  9188  kmlem3  9227  kmlem4  9228  cfub  9324  isf34lem4  9452  grothtsk  9910  suplem1pr  10127  toprntopon  21009  isbasis2g  21032  tgval2  21040  ntreq0  21161  cmpsublem  21482  cmpsub  21483  cmpcld  21485  is1stc2  21525  alexsubALTlem3  22132  alexsubALT  22134  frrlem5c  32230  fnessref  32795  bj-restuni  33478  truniALT  39419  truniALTVD  39766  unisnALT  39814  elunif  39827  ssfiunibd  40162  stoweidlem27  40881  stoweidlem48  40902  setrec1lem3  43105  setrec1  43107
  Copyright terms: Public domain W3C validator