Theorem eluni2 4911

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-uni 4908

This theorem is referenced by:  uni0b  4933  intssuni  4970  iuncom4  5000  inuni  5350  cnvuni  5897  chfnrn  7069  ssorduni  7799  unon  7851  limuni3  7873  frrlem9  8319  onfununi  8381  oarec  8600  uniinqs  8837  fissuni  9397  finsschain  9399  r1sdom  9814  rankuni2b  9893  cflm  10290  coflim  10301  axdc3lem2  10491  fpwwe2lem11  10681  uniwun  10780  tskr1om2  10808  tskuni  10823  axgroth3  10871  inaprc  10876  tskmval  10879  tskmcl  10881  suplem1pr  11092  lbsextlem2  21161  lbsextlem3  21162  isbasis3g  22956  eltg2b  22966  tgcl  22976  ppttop  23014  epttop  23016  neiptoptop  23139  tgcmp  23409  locfincmp  23534  dissnref  23536  comppfsc  23540  1stckgenlem  23561  txuni2  23573  txcmplem1  23649  tgqtop  23720  filuni  23893  alexsubALTlem4  24058  ptcmplem3  24062  ptcmplem4  24063  utoptop  24243  icccmplem1  24844  icccmplem3  24846  cnheibor  24987  bndth  24990  lebnumlem1  24993  bcthlem4  25361  ovolicc2lem5  25556  dyadmbllem  25634  itg2gt0  25795  rexunirn  32511  unipreima  32653  acunirnmpt2  32670  acunirnmpt2f  32671  elrspunidl  33456  ssdifidllem  33484  ssmxidllem  33501  reff  33838  locfinreflem  33839  cmpcref  33849  ddemeas  34237  dya2iocuni  34285  bnj1379  34844  cvmsss2  35279  cvmseu  35281  untuni  35709  dfon2lem3  35786  dfon2lem7  35790  dfon2lem8  35791  brbigcup  35899  neibastop1  36360  neibastop2lem  36361  fvineqsneq  37413  heicant  37662  mblfinlem1  37664  cover2  37722  heiborlem9  37826  unichnidl  38038  erimeq2  38679  prtlem16  38870  prter2  38882  prter3  38883  ssunib  43232  onsupuni  43241  onsuplub  43260  restuni3  45123  disjinfi  45197  cncfuni  45901  intsaluni  46344  salgencntex  46358