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

Theorem eluni 4471
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 3243 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 3243 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 480 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1898 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2718 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 741 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1890 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 4469 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 3385 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 367 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231   cuni 4468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-uni 4469
This theorem is referenced by:  eluni2  4472  elunii  4473  eluniab  4479  uniun  4488  uniin  4489  uniss  4490  unissb  4501  dftr2  4787  unipw  4948  dmuni  5366  fununi  6002  elunirn  6549  uniex2  6994  uniuni  7013  mpt2xopxnop0  7386  wfrfun  7470  wfrlem17  7476  tfrlem7  7524  tfrlem9a  7527  inf2  8558  inf3lem2  8564  rankwflemb  8694  cardprclem  8843  carduni  8845  iunfictbso  8975  kmlem3  9012  kmlem4  9013  cfub  9109  isf34lem4  9237  grothtsk  9695  suplem1pr  9912  toprntopon  20777  isbasis2g  20800  tgval2  20808  ntreq0  20929  cmpsublem  21250  cmpsub  21251  cmpcld  21253  is1stc2  21293  alexsubALTlem3  21900  alexsubALT  21902  frrlem5c  31911  fnessref  32477  bj-restuni  33175  truniALT  39068  truniALTVD  39428  unisnALT  39476  elunif  39489  ssfiunibd  39837  stoweidlem27  40562  stoweidlem48  40583  setrec1lem3  42761  setrec1  42763
  Copyright terms: Public domain W3C validator