Theorem eluni2 4867

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 1862	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4866	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3061	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 303	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-v 3442  df-uni 4864

This theorem is referenced by:  uni0b  4889  intssuni  4925  iuncom4  4955  inuni  5295  cnvuni  5835  chfnrn  6994  ssorduni  7724  unon  7773  limuni3  7794  frrlem9  8236  onfununi  8273  oarec  8489  uniinqs  8734  fissuni  9257  finsschain  9259  r1sdom  9686  rankuni2b  9765  cflm  10160  coflim  10171  axdc3lem2  10361  fpwwe2lem11  10552  uniwun  10651  tskr1om2  10679  tskuni  10694  axgroth3  10742  inaprc  10747  tskmval  10750  tskmcl  10752  suplem1pr  10963  lbsextlem2  21114  lbsextlem3  21115  isbasis3g  22893  eltg2b  22903  tgcl  22913  ppttop  22951  epttop  22953  neiptoptop  23075  tgcmp  23345  locfincmp  23470  dissnref  23472  comppfsc  23476  1stckgenlem  23497  txuni2  23509  txcmplem1  23585  tgqtop  23656  filuni  23829  alexsubALTlem4  23994  ptcmplem3  23998  ptcmplem4  23999  utoptop  24178  icccmplem1  24767  icccmplem3  24769  cnheibor  24910  bndth  24913  lebnumlem1  24916  bcthlem4  25283  ovolicc2lem5  25478  dyadmbllem  25556  itg2gt0  25717  rexunirn  32566  unipreima  32721  acunirnmpt2  32738  acunirnmpt2f  32739  elrspunidl  33509  ssdifidllem  33537  ssmxidllem  33554  reff  33996  locfinreflem  33997  cmpcref  34007  ddemeas  34393  dya2iocuni  34440  bnj1379  34986  cvmsss2  35468  cvmseu  35470  untuni  35903  dfon2lem3  35977  dfon2lem7  35981  dfon2lem8  35982  brbigcup  36090  neibastop1  36553  neibastop2lem  36554  fvineqsneq  37617  heicant  37856  mblfinlem1  37858  cover2  37916  heiborlem9  38020  unichnidl  38232  erimeq2  38937  prtlem16  39129  prter2  39141  prter3  39142  ssunib  43462  onsupuni  43471  onsuplub  43490  restuni3  45362  disjinfi  45436  cncfuni  46130  intsaluni  46573  salgencntex  46587