Theorem eluni 3180

Description: Membership in class union.

Assertion

Ref	Expression
eluni	|- (A e. U.B <-> E.x(A e. x /\ x e. B))

Distinct variable groups:   x,A   x,B

Proof of Theorem eluni

Step	Hyp	Ref	Expression
1		elisset 2299	. 2 |- (A e. U.B -> A e. _V)
2		elisset 2299	. . . 4 |- (A e. x -> A e. _V)
3	2	adantr 425	. . 3 |- ((A e. x /\ x e. B) -> A e. _V)
4	3	19.23aiv 1674	. 2 |- (E.x(A e. x /\ x e. B) -> A e. _V)
5		eleq1 1957	. . . . 5 |- (y = A -> (y e. x <-> A e. x))
6	5	anbi1d 679	. . . 4 |- (y = A -> ((y e. x /\ x e. B) <-> (A e. x /\ x e. B)))
7	6	exbidv 1657	. . 3 |- (y = A -> (E.x(y e. x /\ x e. B) <-> E.x(A e. x /\ x e. B)))
8		df-uni 3178	. . 3 |- U.B = {y | E.x(y e. x /\ x e. B)}
9	7, 8	elab2g 2406	. 2 |- (A e. _V -> (A e. U.B <-> E.x(A e. x /\ x e. B)))
10	1, 4, 9	pm5.21nii 743	1 |- (A e. U.B <-> E.x(A e. x /\ x e. B))

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292  U.cuni 3177

This theorem is referenced by:  eluni2 3181  elunii 3182  hbuni 3183  hbuniOLD 3184  eluniab 3189  uniun 3196  uniin 3197  uniinOLD 3198  uniss 3199  ssuni 3201  ssuniOLD 3202  unissb 3208  iununi 3331  iununiOLD 3332  dftr2 3413  unipw 3504  uniex2 3793  uniuni 3806  dmuni 4166  rnuni 4327  fununi 4481  imaiun 4840  funiunfv 4842  elunirnALT 4845  tfrlem7 5125  uniqs 5354  uniixp 5416  inf2 5714  inf3lem2 5720  truniALT 5845  omsubsdomlem2 5880  kmlem3 5929  kmlem4 5930  unidom 5970  carduni 6010  cfub 6056  suplem1pr 6313  isbasis2g 8881  tgval2 8887  tgss3 8908  basgen 8910  fgbas 10286  extbas1 10291  ordsucuniel 13863  wfrlem11 13967  brbigcup 14074  uninqs 14340  omsubsdomlem2OLD 15389  compsublem 15430  compsub 15431  cptclsscpt 15432  hscptsscld 15434  alexsublem3 15439  alexsub 15441  is1stc3 15469  isfne2 15481  isfne3 15482  fnessref 15503  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  filssufillem 15570  tailuni 15638  totbndss 15937  heiborlem1 15955  prtlem16 16272  truniALTVD 16702

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-uni 3178

Copyright terms: Public domain