Theorem eluni 4867

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.

Step	Hyp	Ref	Expression
1		elex 3474	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3474	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 484	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1949	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2849	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 640	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1940	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4865	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3639	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141  Vcvv 3453  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-uni 4865

This theorem is referenced by:  eluni2  4868  elunii  4869  uniss  4872  eluniab  4878  uniun  4887  uniinOLD  4889  uni0  4893  unissb  4898  dfiun2g  4986  dftr2  5208  unipw  5416  dmuni  5888  iotanul2  6490  fununi  6592  elunirn  7231  uniex2  7717  uniuni  7741  mpoxopxnop0  8190  fprresex  8286  tfrlem7  8349  tfrlem9a  8352  inf2  9575  inf3lem2  9581  rankwflemb  9748  cardprclem  9934  carduni  9936  iunfictbso  10067  kmlem3  10106  kmlem4  10107  cfub  10202  isf34lem4  10331  grothtsk  10790  suplem1pr  11007  toprntopon  22965  isbasis2g  22988  tgval2  22996  ntreq0  23117  cmpsublem  23439  cmpsub  23440  cmpcld  23442  is1stc2  23482  alexsubALTlem3  24089  alexsubALT  24091  elold  27929  fnessref  36681  mh-infprim1bi  36870  bj-restuni  37551  difunieq  37832  ismnushort  44841  truniALT  45081  truniALTVD  45417  unisnALT  45465  uniclaxun  45526  elunif  45560  ssfiunibd  45852  stoweidlem27  46565  stoweidlem48  46586  setrec1lem3  50274  setrec1  50276