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

Theorem eluni 4437
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 3210 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3210 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 481 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1857 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2688 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 741 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1849 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4435 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3351 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 368 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1482  wex 1703  wcel 1989  Vcvv 3198   cuni 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-uni 4435
This theorem is referenced by:  eluni2  4438  elunii  4439  eluniab  4445  uniun  4454  uniin  4455  uniss  4456  unissb  4467  dftr2  4752  unipw  4916  dmuni  5332  fununi  5962  elunirn  6506  uniex2  6949  uniuni  6968  mpt2xopxnop0  7338  wfrfun  7422  wfrlem17  7428  tfrlem7  7476  tfrlem9a  7479  inf2  8517  inf3lem2  8523  rankwflemb  8653  cardprclem  8802  carduni  8804  iunfictbso  8934  kmlem3  8971  kmlem4  8972  cfub  9068  isf34lem4  9196  grothtsk  9654  suplem1pr  9871  toprntopon  20723  isbasis2g  20746  tgval2  20754  ntreq0  20875  cmpsublem  21196  cmpsub  21197  cmpcld  21199  is1stc2  21239  alexsubALTlem3  21847  alexsubALT  21849  frrlem5c  31770  fnessref  32336  bj-restuni  33034  truniALT  38577  truniALTVD  38940  unisnALT  38988  elunif  39001  ssfiunibd  39342  stoweidlem27  40013  stoweidlem48  40034  setrec1lem3  42207  setrec1  42209
  Copyright terms: Public domain W3C validator