Theorem eluni 4843

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 3451	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3451	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 481	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1934	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2827	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 630	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1925	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4841	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3612	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2107  Vcvv 3433  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-uni 4841

This theorem is referenced by:  eluni2  4844  elunii  4845  uniss  4848  eluniab  4855  uniun  4865  uniin  4866  unissb  4874  dfiun2g  4961  dftr2  5194  unipw  5367  dmuni  5826  fununi  6516  elunirn  7133  uniex2  7600  uniuni  7621  mpoxopxnop0  8040  fprresex  8135  wfrfunOLD  8159  wfrlem17OLD  8165  tfrlem7  8223  tfrlem9a  8226  inf2  9390  inf3lem2  9396  rankwflemb  9560  cardprclem  9746  carduni  9748  iunfictbso  9879  kmlem3  9917  kmlem4  9918  cfub  10014  isf34lem4  10142  grothtsk  10600  suplem1pr  10817  toprntopon  22083  isbasis2g  22107  tgval2  22115  ntreq0  22237  cmpsublem  22559  cmpsub  22560  cmpcld  22562  is1stc2  22602  alexsubALTlem3  23209  alexsubALT  23211  elold  34062  fnessref  34555  bj-restuni  35277  difunieq  35554  sn-iotanul  40201  ismnushort  41926  truniALT  42168  truniALTVD  42505  unisnALT  42553  elunif  42566  ssfiunibd  42855  stoweidlem27  43575  stoweidlem48  43596  setrec1lem3  46406  setrec1  46408