Theorem eluni2 4935

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-v 3490  df-uni 4932

This theorem is referenced by:  uni0b  4957  intssuni  4994  iuncom4  5023  inuni  5368  cnvuni  5911  chfnrn  7082  ssorduni  7814  unon  7867  limuni3  7889  frrlem9  8335  onfununi  8397  oarec  8618  uniinqs  8855  fissuni  9427  finsschain  9429  r1sdom  9843  rankuni2b  9922  cflm  10319  coflim  10330  axdc3lem2  10520  fpwwe2lem11  10710  uniwun  10809  tskr1om2  10837  tskuni  10852  axgroth3  10900  inaprc  10905  tskmval  10908  tskmcl  10910  suplem1pr  11121  lbsextlem2  21184  lbsextlem3  21185  isbasis3g  22977  eltg2b  22987  tgcl  22997  ppttop  23035  epttop  23037  neiptoptop  23160  tgcmp  23430  locfincmp  23555  dissnref  23557  comppfsc  23561  1stckgenlem  23582  txuni2  23594  txcmplem1  23670  tgqtop  23741  filuni  23914  alexsubALTlem4  24079  ptcmplem3  24083  ptcmplem4  24084  utoptop  24264  icccmplem1  24863  icccmplem3  24865  cnheibor  25006  bndth  25009  lebnumlem1  25012  bcthlem4  25380  ovolicc2lem5  25575  dyadmbllem  25653  itg2gt0  25815  rexunirn  32520  unipreima  32662  acunirnmpt2  32678  acunirnmpt2f  32679  elrspunidl  33421  ssdifidllem  33449  ssmxidllem  33466  reff  33785  locfinreflem  33786  cmpcref  33796  ddemeas  34200  dya2iocuni  34248  bnj1379  34806  cvmsss2  35242  cvmseu  35244  untuni  35671  dfon2lem3  35749  dfon2lem7  35753  dfon2lem8  35754  brbigcup  35862  neibastop1  36325  neibastop2lem  36326  fvineqsneq  37378  heicant  37615  mblfinlem1  37617  cover2  37675  heiborlem9  37779  unichnidl  37991  erimeq2  38634  prtlem16  38825  prter2  38837  prter3  38838  ssunib  43181  onsupuni  43190  onsuplub  43209  restuni3  45020  disjinfi  45099  cncfuni  45807  intsaluni  46250  salgencntex  46264