Theorem eluni2 4915

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-v 3479  df-uni 4912

This theorem is referenced by:  uni0b  4937  intssuni  4974  iuncom4  5004  inuni  5355  cnvuni  5899  chfnrn  7068  ssorduni  7797  unon  7850  limuni3  7872  frrlem9  8317  onfununi  8379  oarec  8598  uniinqs  8835  fissuni  9394  finsschain  9396  r1sdom  9811  rankuni2b  9890  cflm  10287  coflim  10298  axdc3lem2  10488  fpwwe2lem11  10678  uniwun  10777  tskr1om2  10805  tskuni  10820  axgroth3  10868  inaprc  10873  tskmval  10876  tskmcl  10878  suplem1pr  11089  lbsextlem2  21178  lbsextlem3  21179  isbasis3g  22971  eltg2b  22981  tgcl  22991  ppttop  23029  epttop  23031  neiptoptop  23154  tgcmp  23424  locfincmp  23549  dissnref  23551  comppfsc  23555  1stckgenlem  23576  txuni2  23588  txcmplem1  23664  tgqtop  23735  filuni  23908  alexsubALTlem4  24073  ptcmplem3  24077  ptcmplem4  24078  utoptop  24258  icccmplem1  24857  icccmplem3  24859  cnheibor  25000  bndth  25003  lebnumlem1  25006  bcthlem4  25374  ovolicc2lem5  25569  dyadmbllem  25647  itg2gt0  25809  rexunirn  32519  unipreima  32659  acunirnmpt2  32676  acunirnmpt2f  32677  elrspunidl  33435  ssdifidllem  33463  ssmxidllem  33480  reff  33799  locfinreflem  33800  cmpcref  33810  ddemeas  34216  dya2iocuni  34264  bnj1379  34822  cvmsss2  35258  cvmseu  35260  untuni  35688  dfon2lem3  35766  dfon2lem7  35770  dfon2lem8  35771  brbigcup  35879  neibastop1  36341  neibastop2lem  36342  fvineqsneq  37394  heicant  37641  mblfinlem1  37643  cover2  37701  heiborlem9  37805  unichnidl  38017  erimeq2  38659  prtlem16  38850  prter2  38862  prter3  38863  ssunib  43208  onsupuni  43217  onsuplub  43236  restuni3  45057  disjinfi  45134  cncfuni  45841  intsaluni  46284  salgencntex  46298