Theorem eluni2 4440

Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)

Assertion

Ref	Expression
eluni2	|- ( A e. U. B <-> E. x e. B A e. x )

Distinct variable groups:   x, A   x, B

Proof of Theorem eluni2

Step	Hyp	Ref	Expression
1		exancom 1787	. 2 |- ( E. x ( A e. x /\ x e. B ) <-> E. x ( x e. B /\ A e. x ) )
2		eluni 4439	. 2 |- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )
3		df-rex 2918	. 2 |- ( E. x e. B A e. x <-> E. x ( x e. B /\ A e. x ) )
4	1, 2, 3	3bitr4i 292	1 |- ( A e. U. B <-> E. x e. B A e. x )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704   e. wcel 1990   E.wrex 2913   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-uni 4437

This theorem is referenced by:  uni0b  4463  intssuni  4499  iuncom4  4528  inuni  4826  cnvuni  5309  chfnrn  6328  ssorduni  6985  unon  7031  limuni3  7052  onfununi  7438  oarec  7642  uniinqs  7827  fissuni  8271  finsschain  8273  r1sdom  8637  rankuni2b  8716  cflm  9072  coflim  9083  axdc3lem2  9273  fpwwe2lem12  9463  uniwun  9562  tskr1om2  9590  tskuni  9605  axgroth3  9653  inaprc  9658  tskmval  9661  tskmcl  9663  suplem1pr  9874  lbsextlem2  19159  lbsextlem3  19160  isbasis3g  20753  eltg2b  20763  tgcl  20773  ppttop  20811  epttop  20813  neiptoptop  20935  tgcmp  21204  locfincmp  21329  dissnref  21331  comppfsc  21335  1stckgenlem  21356  txuni2  21368  txcmplem1  21444  tgqtop  21515  filuni  21689  alexsubALTlem4  21854  ptcmplem3  21858  ptcmplem4  21859  utoptop  22038  icccmplem1  22625  icccmplem3  22627  cnheibor  22754  bndth  22757  lebnumlem1  22760  bcthlem4  23124  ovolicc2lem5  23289  dyadmbllem  23367  itg2gt0  23527  rexunirn  29331  unipreima  29446  acunirnmpt2  29460  acunirnmpt2f  29461  reff  29906  locfinreflem  29907  cmpcref  29917  ddemeas  30299  dya2iocuni  30345  bnj1379  30901  cvmsss2  31256  cvmseu  31258  untuni  31586  dfon2lem3  31690  dfon2lem7  31694  dfon2lem8  31695  brbigcup  32005  neibastop1  32354  neibastop2lem  32355  heicant  33444  mblfinlem1  33446  cover2  33508  heiborlem9  33618  unichnidl  33830  prtlem16  34154  prter2  34166  prter3  34167  restuni3  39301  disjinfi  39380  cncfuni  40099  intsaluni  40547  salgencntex  40561