Theorem eluni 4848

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 3453	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3453	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 481	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1937	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2828	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 637	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1928	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4846	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3625	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 379	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3432  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-uni 4846

This theorem is referenced by:  eluni2  4849  elunii  4850  uniss  4853  eluniab  4859  uniun  4868  uniin  4869  uni0  4873  unissb  4878  dfiun2g  4966  dftr2  5188  unipw  5396  dmuni  5863  iotanul2  6465  fununi  6567  elunirn  7202  uniex2  7688  uniuni  7712  mpoxopxnop0  8162  fprresex  8257  tfrlem7  8319  tfrlem9a  8322  inf2  9542  inf3lem2  9548  rankwflemb  9715  cardprclem  9901  carduni  9903  iunfictbso  10034  kmlem3  10073  kmlem4  10074  cfub  10169  isf34lem4  10297  grothtsk  10756  suplem1pr  10973  toprntopon  22915  isbasis2g  22938  tgval2  22946  ntreq0  23067  cmpsublem  23389  cmpsub  23390  cmpcld  23392  is1stc2  23432  alexsubALTlem3  24039  alexsubALT  24041  elold  27876  fnessref  36592  mh-infprim1bi  36781  bj-restuni  37462  difunieq  37743  ismnushort  44752  truniALT  44992  truniALTVD  45328  unisnALT  45376  uniclaxun  45437  elunif  45471  ssfiunibd  45764  stoweidlem27  46477  stoweidlem48  46498  setrec1lem3  50186  setrec1  50188