Theorem eluni2 4835

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 1857	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4834	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3144	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 305	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1776   ∈ wcel 2110  ∃wrex 3139  ∪ cuni 4831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-v 3496  df-uni 4832

This theorem is referenced by:  uni0b  4856  intssuni  4890  iuncom4  4919  inuni  5238  cnvuni  5751  chfnrn  6813  ssorduni  7494  unon  7540  limuni3  7561  onfununi  7972  oarec  8182  uniinqs  8371  fissuni  8823  finsschain  8825  r1sdom  9197  rankuni2b  9276  cflm  9666  coflim  9677  axdc3lem2  9867  fpwwe2lem12  10057  uniwun  10156  tskr1om2  10184  tskuni  10199  axgroth3  10247  inaprc  10252  tskmval  10255  tskmcl  10257  suplem1pr  10468  lbsextlem2  19925  lbsextlem3  19926  isbasis3g  21551  eltg2b  21561  tgcl  21571  ppttop  21609  epttop  21611  neiptoptop  21733  tgcmp  22003  locfincmp  22128  dissnref  22130  comppfsc  22134  1stckgenlem  22155  txuni2  22167  txcmplem1  22243  tgqtop  22314  filuni  22487  alexsubALTlem4  22652  ptcmplem3  22656  ptcmplem4  22657  utoptop  22837  icccmplem1  23424  icccmplem3  23426  cnheibor  23553  bndth  23556  lebnumlem1  23559  bcthlem4  23924  ovolicc2lem5  24116  dyadmbllem  24194  itg2gt0  24355  rexunirn  30250  unipreima  30385  acunirnmpt2  30399  acunirnmpt2f  30400  ssmxidllem  30973  reff  31098  locfinreflem  31099  cmpcref  31109  ddemeas  31490  dya2iocuni  31536  bnj1379  32097  cvmsss2  32516  cvmseu  32518  untuni  32930  dfon2lem3  33025  dfon2lem7  33029  dfon2lem8  33030  frrlem9  33126  brbigcup  33354  neibastop1  33702  neibastop2lem  33703  fvineqsneq  34687  heicant  34921  mblfinlem1  34923  cover2  34983  heiborlem9  35091  unichnidl  35303  erim2  35905  prtlem16  35999  prter2  36011  prter3  36012  restuni3  41377  disjinfi  41447  cncfuni  42162  intsaluni  42606  salgencntex  42620