Theorem eluni2 4862

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057  ∪ cuni 4858

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-v 3439  df-uni 4859

This theorem is referenced by:  uni0b  4884  intssuni  4920  iuncom4  4950  inuni  5290  cnvuni  5830  chfnrn  6988  ssorduni  7718  unon  7767  limuni3  7788  frrlem9  8230  onfununi  8267  oarec  8483  uniinqs  8727  fissuni  9248  finsschain  9250  r1sdom  9674  rankuni2b  9753  cflm  10148  coflim  10159  axdc3lem2  10349  fpwwe2lem11  10539  uniwun  10638  tskr1om2  10666  tskuni  10681  axgroth3  10729  inaprc  10734  tskmval  10737  tskmcl  10739  suplem1pr  10950  lbsextlem2  21098  lbsextlem3  21099  isbasis3g  22865  eltg2b  22875  tgcl  22885  ppttop  22923  epttop  22925  neiptoptop  23047  tgcmp  23317  locfincmp  23442  dissnref  23444  comppfsc  23448  1stckgenlem  23469  txuni2  23481  txcmplem1  23557  tgqtop  23628  filuni  23801  alexsubALTlem4  23966  ptcmplem3  23970  ptcmplem4  23971  utoptop  24150  icccmplem1  24739  icccmplem3  24741  cnheibor  24882  bndth  24885  lebnumlem1  24888  bcthlem4  25255  ovolicc2lem5  25450  dyadmbllem  25528  itg2gt0  25689  rexunirn  32473  unipreima  32627  acunirnmpt2  32644  acunirnmpt2f  32645  elrspunidl  33400  ssdifidllem  33428  ssmxidllem  33445  reff  33873  locfinreflem  33874  cmpcref  33884  ddemeas  34270  dya2iocuni  34317  bnj1379  34863  cvmsss2  35339  cvmseu  35341  untuni  35774  dfon2lem3  35848  dfon2lem7  35852  dfon2lem8  35853  brbigcup  35961  neibastop1  36424  neibastop2lem  36425  fvineqsneq  37477  heicant  37715  mblfinlem1  37717  cover2  37775  heiborlem9  37879  unichnidl  38091  erimeq2  38796  prtlem16  38988  prter2  39000  prter3  39001  ssunib  43337  onsupuni  43346  onsuplub  43365  restuni3  45239  disjinfi  45313  cncfuni  46008  intsaluni  46451  salgencntex  46465