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

Theorem eluni 4369
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 3184 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3184 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 479 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1844 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2675 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 736 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1836 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4367 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3321 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 366 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wex 1694  wcel 1976  Vcvv 3172   cuni 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-uni 4367
This theorem is referenced by:  eluni2  4370  elunii  4371  eluniab  4377  uniun  4386  uniin  4387  uniss  4388  unissb  4399  dftr2  4676  unipw  4839  dmuni  5243  fununi  5864  elunirn  6391  uniex2  6827  uniuni  6842  mpt2xopxnop0  7205  wfrfun  7289  wfrlem17  7295  tfrlem7  7343  tfrlem9a  7346  inf2  8380  inf3lem2  8386  rankwflemb  8516  cardprclem  8665  carduni  8667  iunfictbso  8797  kmlem3  8834  kmlem4  8835  cfub  8931  isf34lem4  9059  grothtsk  9513  suplem1pr  9730  isbasis2g  20505  tgval2  20513  ntreq0  20633  cmpsublem  20954  cmpsub  20955  cmpcld  20957  is1stc2  20997  alexsubALTlem3  21605  alexsubALT  21607  frrlem5c  30836  fnessref  31328  bj-restuni  32027  bj-toprntopon  32040  truniALT  37568  truniALTVD  37932  unisnALT  37980  elunif  37994  ssfiunibd  38260  stoweidlem27  38717  stoweidlem48  38738
  Copyright terms: Public domain W3C validator