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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431  df-uni 4851

This theorem is referenced by:  uni0b  4876  intssuni  4912  iuncom4  4942  inuni  5291  cnvuni  5841  chfnrn  7001  ssorduni  7733  unon  7782  limuni3  7803  frrlem9  8244  onfununi  8281  oarec  8497  uniinqs  8744  fissuni  9267  finsschain  9269  r1sdom  9698  rankuni2b  9777  cflm  10172  coflim  10183  axdc3lem2  10373  fpwwe2lem11  10564  uniwun  10663  tskr1om2  10691  tskuni  10706  axgroth3  10754  inaprc  10759  tskmval  10762  tskmcl  10764  suplem1pr  10975  lbsextlem2  21157  lbsextlem3  21158  isbasis3g  22914  eltg2b  22924  tgcl  22934  ppttop  22972  epttop  22974  neiptoptop  23096  tgcmp  23366  locfincmp  23491  dissnref  23493  comppfsc  23497  1stckgenlem  23518  txuni2  23530  txcmplem1  23606  tgqtop  23677  filuni  23850  alexsubALTlem4  24015  ptcmplem3  24019  ptcmplem4  24020  utoptop  24199  icccmplem1  24788  icccmplem3  24790  cnheibor  24922  bndth  24925  lebnumlem1  24928  bcthlem4  25294  ovolicc2lem5  25488  dyadmbllem  25566  itg2gt0  25727  rexunirn  32561  unipreima  32716  acunirnmpt2  32733  acunirnmpt2f  32734  elrspunidl  33488  ssdifidllem  33516  ssmxidllem  33533  reff  33983  locfinreflem  33984  cmpcref  33994  ddemeas  34380  dya2iocuni  34427  bnj1379  34972  cvmsss2  35456  cvmseu  35458  untuni  35891  dfon2lem3  35965  dfon2lem7  35969  dfon2lem8  35970  brbigcup  36078  neibastop1  36541  neibastop2lem  36542  fvineqsneq  37728  heicant  37976  mblfinlem1  37978  cover2  38036  heiborlem9  38140  unichnidl  38352  erimeq2  39084  prtlem16  39315  prter2  39327  prter3  39328  ssunib  43648  onsupuni  43657  onsuplub  43676  restuni3  45548  disjinfi  45622  cncfuni  46314  intsaluni  46757  salgencntex  46771