Theorem eluni2 4887

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-uni 4884

This theorem is referenced by:  uni0b  4909  intssuni  4946  iuncom4  4976  inuni  5320  cnvuni  5866  chfnrn  7039  ssorduni  7773  unon  7825  limuni3  7847  frrlem9  8293  onfununi  8355  oarec  8574  uniinqs  8811  fissuni  9369  finsschain  9371  r1sdom  9788  rankuni2b  9867  cflm  10264  coflim  10275  axdc3lem2  10465  fpwwe2lem11  10655  uniwun  10754  tskr1om2  10782  tskuni  10797  axgroth3  10845  inaprc  10850  tskmval  10853  tskmcl  10855  suplem1pr  11066  lbsextlem2  21120  lbsextlem3  21121  isbasis3g  22887  eltg2b  22897  tgcl  22907  ppttop  22945  epttop  22947  neiptoptop  23069  tgcmp  23339  locfincmp  23464  dissnref  23466  comppfsc  23470  1stckgenlem  23491  txuni2  23503  txcmplem1  23579  tgqtop  23650  filuni  23823  alexsubALTlem4  23988  ptcmplem3  23992  ptcmplem4  23993  utoptop  24173  icccmplem1  24762  icccmplem3  24764  cnheibor  24905  bndth  24908  lebnumlem1  24911  bcthlem4  25279  ovolicc2lem5  25474  dyadmbllem  25552  itg2gt0  25713  rexunirn  32473  unipreima  32621  acunirnmpt2  32638  acunirnmpt2f  32639  elrspunidl  33443  ssdifidllem  33471  ssmxidllem  33488  reff  33870  locfinreflem  33871  cmpcref  33881  ddemeas  34267  dya2iocuni  34315  bnj1379  34861  cvmsss2  35296  cvmseu  35298  untuni  35726  dfon2lem3  35803  dfon2lem7  35807  dfon2lem8  35808  brbigcup  35916  neibastop1  36377  neibastop2lem  36378  fvineqsneq  37430  heicant  37679  mblfinlem1  37681  cover2  37739  heiborlem9  37843  unichnidl  38055  erimeq2  38696  prtlem16  38887  prter2  38899  prter3  38900  ssunib  43244  onsupuni  43253  onsuplub  43272  restuni3  45142  disjinfi  45216  cncfuni  45915  intsaluni  46358  salgencntex  46372