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

Theorem eluni 4575
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 3361 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3361 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 466 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 2009 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2837 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 607 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 2001 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4573 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3502 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 367 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1630  wex 1851  wcel 2144  Vcvv 3349   cuni 4572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-uni 4573
This theorem is referenced by:  eluni2  4576  elunii  4577  eluniab  4583  uniun  4591  uniin  4592  uniss  4593  unissb  4603  dftr2  4886  unipw  5046  dmuni  5472  fununi  6104  elunirn  6651  uniex2  7098  uniuni  7117  mpt2xopxnop0  7492  wfrfun  7577  wfrlem17  7583  tfrlem7  7631  tfrlem9a  7634  inf2  8683  inf3lem2  8689  rankwflemb  8819  cardprclem  9004  carduni  9006  iunfictbso  9136  kmlem3  9175  kmlem4  9176  cfub  9272  isf34lem4  9400  grothtsk  9858  suplem1pr  10075  toprntopon  20949  isbasis2g  20972  tgval2  20980  ntreq0  21101  cmpsublem  21422  cmpsub  21423  cmpcld  21425  is1stc2  21465  alexsubALTlem3  22072  alexsubALT  22074  frrlem5c  32117  fnessref  32683  bj-restuni  33375  truniALT  39270  truniALTVD  39630  unisnALT  39678  elunif  39691  ssfiunibd  40034  stoweidlem27  40755  stoweidlem48  40776  setrec1lem3  42954  setrec1  42956
  Copyright terms: Public domain W3C validator