Theorem eluni2 4809

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 1869	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4808	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3057	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 306	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1787   ∈ wcel 2112  ∃wrex 3052  ∪ cuni 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rex 3057  df-v 3400  df-uni 4806

This theorem is referenced by:  uni0b  4833  intssuni  4867  iuncom4  4898  inuni  5221  cnvuni  5740  chfnrn  6847  ssorduni  7541  unon  7588  limuni3  7609  frrlem9  8013  onfununi  8056  oarec  8268  uniinqs  8457  fissuni  8959  finsschain  8961  r1sdom  9355  rankuni2b  9434  cflm  9829  coflim  9840  axdc3lem2  10030  fpwwe2lem11  10220  uniwun  10319  tskr1om2  10347  tskuni  10362  axgroth3  10410  inaprc  10415  tskmval  10418  tskmcl  10420  suplem1pr  10631  lbsextlem2  20150  lbsextlem3  20151  isbasis3g  21800  eltg2b  21810  tgcl  21820  ppttop  21858  epttop  21860  neiptoptop  21982  tgcmp  22252  locfincmp  22377  dissnref  22379  comppfsc  22383  1stckgenlem  22404  txuni2  22416  txcmplem1  22492  tgqtop  22563  filuni  22736  alexsubALTlem4  22901  ptcmplem3  22905  ptcmplem4  22906  utoptop  23086  icccmplem1  23673  icccmplem3  23675  cnheibor  23806  bndth  23809  lebnumlem1  23812  bcthlem4  24178  ovolicc2lem5  24372  dyadmbllem  24450  itg2gt0  24612  rexunirn  30513  unipreima  30654  acunirnmpt2  30671  acunirnmpt2f  30672  elrspunidl  31274  ssmxidllem  31309  reff  31457  locfinreflem  31458  cmpcref  31468  ddemeas  31870  dya2iocuni  31916  bnj1379  32477  cvmsss2  32903  cvmseu  32905  untuni  33317  dfon2lem3  33431  dfon2lem7  33435  dfon2lem8  33436  brbigcup  33886  neibastop1  34234  neibastop2lem  34235  fvineqsneq  35269  heicant  35498  mblfinlem1  35500  cover2  35558  heiborlem9  35663  unichnidl  35875  erim2  36475  prtlem16  36569  prter2  36581  prter3  36582  restuni3  42281  disjinfi  42345  cncfuni  43045  intsaluni  43486  salgencntex  43500