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

Theorem eluni 4375
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 3185 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3185 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 480 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1845 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2676 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 737 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1837 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4373 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3322 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 367 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383   = wceq 1475  wex 1695  wcel 1977  Vcvv 3173   cuni 4372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-uni 4373
This theorem is referenced by:  eluni2  4376  elunii  4377  eluniab  4383  uniun  4392  uniin  4393  uniss  4394  unissb  4405  dftr2  4682  unipw  4845  dmuni  5256  fununi  5878  elunirn  6413  uniex2  6850  uniuni  6865  mpt2xopxnop0  7228  wfrfun  7312  wfrlem17  7318  tfrlem7  7366  tfrlem9a  7369  inf2  8403  inf3lem2  8409  rankwflemb  8539  cardprclem  8688  carduni  8690  iunfictbso  8820  kmlem3  8857  kmlem4  8858  cfub  8954  isf34lem4  9082  grothtsk  9536  suplem1pr  9753  isbasis2g  20563  tgval2  20571  ntreq0  20691  cmpsublem  21012  cmpsub  21013  cmpcld  21015  is1stc2  21055  alexsubALTlem3  21663  alexsubALT  21665  frrlem5c  31030  fnessref  31522  bj-restuni  32231  bj-toprntopon  32244  truniALT  37772  truniALTVD  38136  unisnALT  38184  elunif  38198  ssfiunibd  38464  stoweidlem27  38920  stoweidlem48  38941  setrec1lem3  42235  setrec1  42237
  Copyright terms: Public domain W3C validator