Theorem eluni 4869

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 3471	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3471	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 486	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1962	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2848	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 643	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1953	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4867	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-uni 4867

This theorem is used by:  eluni2  4870  elunii  4871  uniss  4874  eluniab  4880  uniun  4889  uniinOLD  4891  uni0  4895  unissb  4900  dfiun2g  4987  dftr2  5213  unipw  5417  dmuni  5895  iotanul2  6511  fununi  6616  elunirn  7256  uniex2  7755  uniex2OLD  7756  uniuni  7777  mpoxopxnop0  8236  fprresex  8332  tfrlem7  8395  tfrlem9a  8398  inf2  9628  inf3lem2  9634  rankwflemb  9804  rankwflembOLD  9805  setrec1lem3  9973  setrec1  9976  cardprclem  10064  carduni  10066  iunfictbso  10197  kmlem3  10235  kmlem4  10236  cfub  10330  isf34lem4  10459  grothtsk  10924  suplem1pr  11141  lidlunin0  21521  toprntopon  23249  isbasis2g  23272  tgval2  23280  ntreq0  23401  cmpsublem  23723  cmpsub  23724  cmpcld  23726  is1stc2  23766  alexsubALTlem3  24374  alexsubALT  24376  elold  28251  fnessref  37238  mh-infprim1bi  37427  bj-restuni  38111  difunieq  38391  ismnushort  45379  truniALT  45618  truniALTVD  45954  unisnALT  46002  uniclaxun  46070  elunif  46127  ssfiunibd  46419  stoweidlem27  47131  stoweidlem48  47152