Theorem eluni2 4877

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 1891	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4876	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3090	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 306	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-v 3457  df-uni 4874

This theorem is referenced by:  uni0b  4900  intssuni  4936  iuncom4  4966  inuni  5322  cnvuni  5878  chfnrn  7046  ssorduni  7779  unon  7828  limuni3  7849  frrlem9  8292  onfununi  8329  oarec  8548  uniinqs  8796  fissuni  9315  finsschain  9317  r1sdom  9747  rankuni2b  9826  cflm  10234  coflim  10246  axdc3lem2  10436  fpwwe2lem11  10627  uniwun  10726  tskr1om2  10754  tskuni  10769  axgroth3  10817  inaprc  10822  tskmval  10825  tskmcl  10827  suplem1pr  11038  lbsextlem2  21264  lbsextlem3  21265  unichnlidl  21343  ssdifidllem  21465  isbasis3g  23087  eltg2b  23097  tgcl  23107  ppttop  23145  epttop  23147  neiptoptop  23269  tgcmp  23539  locfincmp  23664  dissnref  23666  comppfsc  23670  1stckgenlem  23691  txuni2  23703  txcmplem1  23779  tgqtop  23850  filuni  24023  alexsubALTlem4  24188  ptcmplem3  24192  ptcmplem4  24193  utoptop  24372  icccmplem1  24961  icccmplem3  24963  cnheibor  25095  bndth  25098  lebnumlem1  25101  bcthlem4  25467  ovolicc2lem5  25661  dyadmbllem  25739  itg2gt0  25900  rexunirn  32819  unipreima  32969  acunirnmpt2  32986  acunirnmpt2f  32987  elrspunidl  33717  ssmxidllem  33737  reff  34210  locfinreflem  34211  cmpcref  34221  ddemeas  34607  dya2iocuni  34654  bnj1379  35199  cvmsss2  35747  cvmseu  35749  untuni  36182  dfon2lem3  36256  dfon2lem7  36260  dfon2lem8  36261  brbigcup  36369  neibastop1  36851  neibastop2lem  36852  fvineqsneq  38039  heicant  38287  mblfinlem1  38289  cover2  38347  heiborlem9  38451  unichnidl  38663  erimeq2  39393  prtlem16  39624  prter2  39636  prter3  39637  ssunib  43930  onsupuni  43939  onsuplub  43958  restuni3  45819  disjinfi  45893  cncfuni  46583  intsaluni  47026  salgencntex  47040