Theorem eluni2 4913

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

Assertion

Ref	Expression
eluni2	⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eluni2

Step	Hyp	Ref	Expression
1		exancom 1865	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4912	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 303	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-uni 4910

This theorem is referenced by:  uni0b  4938  intssuni  4975  iuncom4  5006  inuni  5344  cnvuni  5887  chfnrn  7051  ssorduni  7766  unon  7819  limuni3  7841  frrlem9  8279  onfununi  8341  oarec  8562  uniinqs  8791  fissuni  9357  finsschain  9359  r1sdom  9769  rankuni2b  9848  cflm  10245  coflim  10256  axdc3lem2  10446  fpwwe2lem11  10636  uniwun  10735  tskr1om2  10763  tskuni  10778  axgroth3  10826  inaprc  10831  tskmval  10834  tskmcl  10836  suplem1pr  11047  lbsextlem2  20772  lbsextlem3  20773  isbasis3g  22452  eltg2b  22462  tgcl  22472  ppttop  22510  epttop  22512  neiptoptop  22635  tgcmp  22905  locfincmp  23030  dissnref  23032  comppfsc  23036  1stckgenlem  23057  txuni2  23069  txcmplem1  23145  tgqtop  23216  filuni  23389  alexsubALTlem4  23554  ptcmplem3  23558  ptcmplem4  23559  utoptop  23739  icccmplem1  24338  icccmplem3  24340  cnheibor  24471  bndth  24474  lebnumlem1  24477  bcthlem4  24844  ovolicc2lem5  25038  dyadmbllem  25116  itg2gt0  25278  rexunirn  31732  unipreima  31869  acunirnmpt2  31885  acunirnmpt2f  31886  elrspunidl  32546  ssmxidllem  32589  reff  32819  locfinreflem  32820  cmpcref  32830  ddemeas  33234  dya2iocuni  33282  bnj1379  33841  cvmsss2  34265  cvmseu  34267  untuni  34678  dfon2lem3  34757  dfon2lem7  34761  dfon2lem8  34762  brbigcup  34870  neibastop1  35244  neibastop2lem  35245  fvineqsneq  36293  heicant  36523  mblfinlem1  36525  cover2  36583  heiborlem9  36687  unichnidl  36899  erimeq2  37548  prtlem16  37739  prter2  37751  prter3  37752  ssunib  41969  onsupuni  41978  onsuplub  41997  restuni3  43807  disjinfi  43891  cncfuni  44602  intsaluni  45045  salgencntex  45059