Theorem eluni 4874

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 3468	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3468	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 480	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1930	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2816	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 631	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1921	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4872	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3647	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3447  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-uni 4872

This theorem is referenced by:  eluni2  4875  elunii  4876  uniss  4879  eluniab  4885  uniun  4894  uniin  4895  unissb  4903  unissbOLD  4904  dfiun2g  4994  dftr2  5216  unipw  5410  dmuni  5878  iotanul2  6481  fununi  6591  elunirn  7225  uniex2  7714  uniuni  7738  mpoxopxnop0  8194  fprresex  8289  tfrlem7  8351  tfrlem9a  8354  inf2  9576  inf3lem2  9582  rankwflemb  9746  cardprclem  9932  carduni  9934  iunfictbso  10067  kmlem3  10106  kmlem4  10107  cfub  10202  isf34lem4  10330  grothtsk  10788  suplem1pr  11005  toprntopon  22812  isbasis2g  22835  tgval2  22843  ntreq0  22964  cmpsublem  23286  cmpsub  23287  cmpcld  23289  is1stc2  23329  alexsubALTlem3  23936  alexsubALT  23938  elold  27781  fnessref  36345  bj-restuni  37085  difunieq  37362  ismnushort  44290  truniALT  44531  truniALTVD  44867  unisnALT  44915  uniclaxun  44976  elunif  45010  ssfiunibd  45307  stoweidlem27  46025  stoweidlem48  46046  setrec1lem3  49678  setrec1  49680