Theorem eluni 4871

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 3478	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3478	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 485	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1953	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2853	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 642	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1944	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4869	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3642	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 381	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  Vcvv 3457  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-uni 4869

This theorem is referenced by:  eluni2  4872  elunii  4873  uniss  4876  eluniab  4882  uniun  4891  uniinOLD  4893  uni0  4897  unissb  4902  dfiun2g  4990  dftr2  5214  unipw  5422  dmuni  5895  iotanul2  6498  fununi  6600  elunirn  7239  uniex2  7725  uniuni  7749  mpoxopxnop0  8199  fprresex  8295  tfrlem7  8358  tfrlem9a  8361  inf2  9580  inf3lem2  9586  rankwflemb  9753  cardprclem  9953  carduni  9955  iunfictbso  10086  kmlem3  10124  kmlem4  10125  cfub  10220  isf34lem4  10349  grothtsk  10808  suplem1pr  11025  lidlunin0  21330  toprntopon  23043  isbasis2g  23066  tgval2  23074  ntreq0  23195  cmpsublem  23517  cmpsub  23518  cmpcld  23520  is1stc2  23560  alexsubALTlem3  24167  alexsubALT  24169  elold  28010  fnessref  36730  mh-infprim1bi  36919  bj-restuni  37599  difunieq  37880  ismnushort  44875  truniALT  45115  truniALTVD  45451  unisnALT  45499  uniclaxun  45560  elunif  45594  ssfiunibd  45886  stoweidlem27  46599  stoweidlem48  46620  setrec1lem3  50318  setrec1  50320