Theorem eluni 4833

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 3511	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 3511	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 483	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1925	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2898	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 631	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1916	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 4831	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 3666	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 382	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1531  ∃wex 1774   ∈ wcel 2108  Vcvv 3493  ∪ cuni 4830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-uni 4831

This theorem is referenced by:  eluni2  4834  elunii  4835  eluniab  4841  uniun  4849  uniin  4850  uniss  4851  unissb  4861  dftr2  5165  unipw  5333  dmuni  5776  fununi  6422  elunirn  7002  uniex2  7456  uniuni  7476  mpoxopxnop0  7873  wfrfun  7957  wfrlem17  7963  tfrlem7  8011  tfrlem9a  8014  inf2  9078  inf3lem2  9084  rankwflemb  9214  cardprclem  9400  carduni  9402  iunfictbso  9532  kmlem3  9570  kmlem4  9571  cfub  9663  isf34lem4  9791  grothtsk  10249  suplem1pr  10466  toprntopon  21525  isbasis2g  21548  tgval2  21556  ntreq0  21677  cmpsublem  21999  cmpsub  22000  cmpcld  22002  is1stc2  22042  alexsubALTlem3  22649  alexsubALT  22651  fnessref  33698  bj-restuni  34380  difunieq  34647  truniALT  40865  truniALTVD  41202  unisnALT  41250  elunif  41263  ssfiunibd  41565  stoweidlem27  42302  stoweidlem48  42323  setrec1lem3  44782  setrec1  44784