Theorem eluni 4868

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 3463	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3463	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 480	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1932	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2825	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 632	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1923	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4866	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3637	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3442  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-uni 4866

This theorem is referenced by:  eluni2  4869  elunii  4870  uniss  4873  eluniab  4879  uniun  4888  uniin  4889  uni0  4893  unissb  4898  dfiun2g  4987  dftr2  5209  unipw  5405  dmuni  5871  iotanul2  6473  fununi  6575  elunirn  7207  uniex2  7693  uniuni  7717  mpoxopxnop0  8167  fprresex  8262  tfrlem7  8324  tfrlem9a  8327  inf2  9544  inf3lem2  9550  rankwflemb  9717  cardprclem  9903  carduni  9905  iunfictbso  10036  kmlem3  10075  kmlem4  10076  cfub  10171  isf34lem4  10299  grothtsk  10758  suplem1pr  10975  toprntopon  22881  isbasis2g  22904  tgval2  22912  ntreq0  23033  cmpsublem  23355  cmpsub  23356  cmpcld  23358  is1stc2  23398  alexsubALTlem3  24005  alexsubALT  24007  elold  27867  fnessref  36570  bj-restuni  37344  difunieq  37623  ismnushort  44651  truniALT  44891  truniALTVD  45227  unisnALT  45275  uniclaxun  45336  elunif  45370  ssfiunibd  45665  stoweidlem27  46379  stoweidlem48  46400  setrec1lem3  50042  setrec1  50044