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

Theorem eluni 4807
 Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eluni
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3460 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3460 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 484 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1931 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 elequ1 2118 . . . . 5 (𝑦 = 𝑧 → (𝑦𝑥𝑧𝑥))
65anbi1d 632 . . . 4 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝐵) ↔ (𝑧𝑥𝑥𝐵)))
76exbidv 1922 . . 3 (𝑦 = 𝑧 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝑧𝑥𝑥𝐵)))
8 eleq1 2877 . . . . 5 (𝑧 = 𝐴 → (𝑧𝑥𝐴𝑥))
98anbi1d 632 . . . 4 (𝑧 = 𝐴 → ((𝑧𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
109exbidv 1922 . . 3 (𝑧 = 𝐴 → (∃𝑥(𝑧𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
11 df-uni 4805 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
127, 10, 11elab2gw 3614 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
131, 4, 12pm5.21nii 383 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3442  ∪ cuni 4804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-uni 4805 This theorem is referenced by:  eluni2  4808  elunii  4809  uniss  4812  eluniab  4819  uniun  4827  uniin  4828  unissb  4836  dftr2  5142  unipw  5312  dmuni  5753  fununi  6407  elunirn  6998  uniex2  7457  uniuni  7477  mpoxopxnop0  7882  wfrfun  7966  wfrlem17  7972  tfrlem7  8020  tfrlem9a  8023  inf2  9088  inf3lem2  9094  rankwflemb  9224  cardprclem  9410  carduni  9412  iunfictbso  9543  kmlem3  9581  kmlem4  9582  cfub  9678  isf34lem4  9806  grothtsk  10264  suplem1pr  10481  toprntopon  21571  isbasis2g  21594  tgval2  21602  ntreq0  21723  cmpsublem  22045  cmpsub  22046  cmpcld  22048  is1stc2  22088  alexsubALTlem3  22695  alexsubALT  22697  elold  33530  fnessref  33965  bj-restuni  34663  difunieq  34942  truniALT  41418  truniALTVD  41755  unisnALT  41803  elunif  41816  ssfiunibd  42109  stoweidlem27  42837  stoweidlem48  42858  setrec1lem3  45385  setrec1  45387
 Copyright terms: Public domain W3C validator