Theorem eluni2 4854

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 1863	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4853	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 302	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1780   ∈ wcel 2105  ∃wrex 3071  ∪ cuni 4850

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-v 3443  df-uni 4851

This theorem is referenced by:  uni0b  4879  intssuni  4914  iuncom4  4945  inuni  5282  cnvuni  5815  chfnrn  6965  ssorduni  7669  unon  7721  limuni3  7743  frrlem9  8157  onfununi  8219  oarec  8441  uniinqs  8634  fissuni  9194  finsschain  9196  r1sdom  9603  rankuni2b  9682  cflm  10079  coflim  10090  axdc3lem2  10280  fpwwe2lem11  10470  uniwun  10569  tskr1om2  10597  tskuni  10612  axgroth3  10660  inaprc  10665  tskmval  10668  tskmcl  10670  suplem1pr  10881  lbsextlem2  20493  lbsextlem3  20494  isbasis3g  22171  eltg2b  22181  tgcl  22191  ppttop  22229  epttop  22231  neiptoptop  22354  tgcmp  22624  locfincmp  22749  dissnref  22751  comppfsc  22755  1stckgenlem  22776  txuni2  22788  txcmplem1  22864  tgqtop  22935  filuni  23108  alexsubALTlem4  23273  ptcmplem3  23277  ptcmplem4  23278  utoptop  23458  icccmplem1  24057  icccmplem3  24059  cnheibor  24190  bndth  24193  lebnumlem1  24196  bcthlem4  24563  ovolicc2lem5  24757  dyadmbllem  24835  itg2gt0  24997  rexunirn  30949  unipreima  31089  acunirnmpt2  31105  acunirnmpt2f  31106  elrspunidl  31711  ssmxidllem  31746  reff  31895  locfinreflem  31896  cmpcref  31906  ddemeas  32310  dya2iocuni  32356  bnj1379  32915  cvmsss2  33341  cvmseu  33343  untuni  33755  dfon2lem3  33860  dfon2lem7  33864  dfon2lem8  33865  brbigcup  34258  neibastop1  34606  neibastop2lem  34607  fvineqsneq  35639  heicant  35868  mblfinlem1  35870  cover2  35928  heiborlem9  36033  unichnidl  36245  erimeq2  36896  prtlem16  37087  prter2  37099  prter3  37100  restuni3  42889  disjinfi  42959  cncfuni  43664  intsaluni  44105  salgencntex  44119