Theorem eluni 2572

Description: Membership in class union.

Assertion

Ref	Expression
eluni	⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ⋀ x ∈ B))

Distinct variable groups:   x,A   x,B

Proof of Theorem eluni

Step	Hyp	Ref	Expression
1		elisset 1863	. 2 ⊢ (A ∈ ∪B → A ∈ V)
2		elisset 1863	. . . 4 ⊢ (A ∈ x → A ∈ V)
3	2	adantr 389	. . 3 ⊢ ((A ∈ x ⋀ x ∈ B) → A ∈ V)
4	3	19.23aiv 1333	. 2 ⊢ (∃x(A ∈ x ⋀ x ∈ B) → A ∈ V)
5		eleq1 1577	. . . . 5 ⊢ (y = A → (y ∈ x ↔ A ∈ x))
6	5	anbi1d 620	. . . 4 ⊢ (y = A → ((y ∈ x ⋀ x ∈ B) ↔ (A ∈ x ⋀ x ∈ B)))
7	6	exbidv 1317	. . 3 ⊢ (y = A → (∃x(y ∈ x ⋀ x ∈ B) ↔ ∃x(A ∈ x ⋀ x ∈ B)))
8		df-uni 2570	. . 3 ⊢ ∪B = {y∣∃x(y ∈ x ⋀ x ∈ B)}
9	7, 8	elab2g 1946	. 2 ⊢ (A ∈ V → (A ∈ ∪B ↔ ∃x(A ∈ x ⋀ x ∈ B)))
10	1, 4, 9	pm5.21nii 683	1 ⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ⋀ x ∈ B))

Syntax hints:   ↔ wb 144   ⋀ wa 221   = wceq 992   ∈ wcel 994  ∃wex 1016  Vcvv 1857  ∪cuni 2569

This theorem is referenced by:  eluni2 2573  elunii 2574  hbuni 2575  eluniab 2579  uniun 2586  uniin 2587  ssuni 2589  unissb 2595  iununi 2686  dftr2 2756  unipw 2836  uniex2 3092  uniuni 3104  dmuni 3410  rnuni 3544  fununi 3668  imaiun 3978  funiunfv 3980  elunirnALT 3983  tfrlem7 4218  uniqs 4436  uniixp 4498  inf2 4753  inf3lem2 4759  kmlem3 4913  kmlem4 4914  unidom 4954  carduni 5008  cfub 5058  suplem1pr 5315  isbasis2g 7824  tgval2 7829  tgss3 7850  basgen 7852  uninqs 10730  omsubsdomlem2 11441  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  alexsublem3 11498  alexsub 11500  is1stc3 11530  isfne2 11542  isfne3 11543  fnessref 11564  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  fgbas 11636  extbas1 11641  filssufillem 11655  tailuni 11761  metsstop 11909  totbndss 11993  heiborlem1 12011

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-uni 2570

Copyright terms: Public domain