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

Theorem eluni 4822
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 3426 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3426 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 484 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1938 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2825 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 633 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1929 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4820 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3589 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 383 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1543  wex 1787  wcel 2110  Vcvv 3408   cuni 4819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-uni 4820
This theorem is referenced by:  eluni2  4823  elunii  4824  uniss  4827  eluniab  4834  uniun  4844  uniin  4845  unissb  4853  dftr2  5163  unipw  5335  dmuni  5783  fununi  6455  elunirn  7064  uniex2  7526  uniuni  7547  mpoxopxnop0  7957  wfrfun  8065  wfrlem17  8071  tfrlem7  8119  tfrlem9a  8122  inf2  9238  inf3lem2  9244  rankwflemb  9409  cardprclem  9595  carduni  9597  iunfictbso  9728  kmlem3  9766  kmlem4  9767  cfub  9863  isf34lem4  9991  grothtsk  10449  suplem1pr  10666  toprntopon  21822  isbasis2g  21845  tgval2  21853  ntreq0  21974  cmpsublem  22296  cmpsub  22297  cmpcld  22299  is1stc2  22339  alexsubALTlem3  22946  alexsubALT  22948  elold  33790  fnessref  34283  bj-restuni  35003  difunieq  35282  ismnushort  41592  truniALT  41834  truniALTVD  42171  unisnALT  42219  elunif  42232  ssfiunibd  42521  stoweidlem27  43243  stoweidlem48  43264  setrec1lem3  46066  setrec1  46068
  Copyright terms: Public domain W3C validator