Theorem eluni2 4849

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 1868	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4848	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 304	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-v 3434  df-uni 4846

This theorem is referenced by:  uni0b  4871  intssuni  4907  iuncom4  4937  inuni  5285  cnvuni  5835  chfnrn  6997  ssorduni  7729  unon  7778  limuni3  7799  frrlem9  8241  onfununi  8278  oarec  8494  uniinqs  8741  fissuni  9264  finsschain  9266  r1sdom  9696  rankuni2b  9775  cflm  10170  coflim  10181  axdc3lem2  10371  fpwwe2lem11  10562  uniwun  10661  tskr1om2  10689  tskuni  10704  axgroth3  10752  inaprc  10757  tskmval  10760  tskmcl  10762  suplem1pr  10973  lbsextlem2  21159  lbsextlem3  21160  isbasis3g  22939  eltg2b  22949  tgcl  22959  ppttop  22997  epttop  22999  neiptoptop  23121  tgcmp  23391  locfincmp  23516  dissnref  23518  comppfsc  23522  1stckgenlem  23543  txuni2  23555  txcmplem1  23631  tgqtop  23702  filuni  23875  alexsubALTlem4  24040  ptcmplem3  24044  ptcmplem4  24045  utoptop  24224  icccmplem1  24813  icccmplem3  24815  cnheibor  24947  bndth  24950  lebnumlem1  24953  bcthlem4  25319  ovolicc2lem5  25513  dyadmbllem  25591  itg2gt0  25752  rexunirn  32586  unipreima  32742  acunirnmpt2  32759  acunirnmpt2f  32760  elrspunidl  33518  ssdifidllem  33546  ssmxidllem  33563  reff  34030  locfinreflem  34031  cmpcref  34041  ddemeas  34427  dya2iocuni  34474  bnj1379  35019  cvmsss2  35509  cvmseu  35511  untuni  35944  dfon2lem3  36018  dfon2lem7  36022  dfon2lem8  36023  brbigcup  36131  neibastop1  36594  neibastop2lem  36595  fvineqsneq  37781  heicant  38029  mblfinlem1  38031  cover2  38089  heiborlem9  38193  unichnidl  38405  erimeq2  39137  prtlem16  39368  prter2  39380  prter3  39381  ssunib  43672  onsupuni  43681  onsuplub  43700  restuni3  45572  disjinfi  45646  cncfuni  46336  intsaluni  46779  salgencntex  46793