Theorem eluni2 4472

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 1827	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4471	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 2947	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 292	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744   ∈ wcel 2030  ∃wrex 2942  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-uni 4469

This theorem is referenced by:  uni0b  4495  intssuni  4531  iuncom4  4560  inuni  4856  cnvuni  5341  chfnrn  6368  ssorduni  7027  unon  7073  limuni3  7094  onfununi  7483  oarec  7687  uniinqs  7870  fissuni  8312  finsschain  8314  r1sdom  8675  rankuni2b  8754  cflm  9110  coflim  9121  axdc3lem2  9311  fpwwe2lem12  9501  uniwun  9600  tskr1om2  9628  tskuni  9643  axgroth3  9691  inaprc  9696  tskmval  9699  tskmcl  9701  suplem1pr  9912  lbsextlem2  19207  lbsextlem3  19208  isbasis3g  20801  eltg2b  20811  tgcl  20821  ppttop  20859  epttop  20861  neiptoptop  20983  tgcmp  21252  locfincmp  21377  dissnref  21379  comppfsc  21383  1stckgenlem  21404  txuni2  21416  txcmplem1  21492  tgqtop  21563  filuni  21736  alexsubALTlem4  21901  ptcmplem3  21905  ptcmplem4  21906  utoptop  22085  icccmplem1  22672  icccmplem3  22674  cnheibor  22801  bndth  22804  lebnumlem1  22807  bcthlem4  23170  ovolicc2lem5  23335  dyadmbllem  23413  itg2gt0  23572  rexunirn  29458  unipreima  29574  acunirnmpt2  29588  acunirnmpt2f  29589  reff  30034  locfinreflem  30035  cmpcref  30045  ddemeas  30427  dya2iocuni  30473  bnj1379  31027  cvmsss2  31382  cvmseu  31384  untuni  31712  dfon2lem3  31814  dfon2lem7  31818  dfon2lem8  31819  brbigcup  32130  neibastop1  32479  neibastop2lem  32480  heicant  33574  mblfinlem1  33576  cover2  33638  heiborlem9  33748  unichnidl  33960  prtlem16  34473  prter2  34485  prter3  34486  restuni3  39615  disjinfi  39694  cncfuni  40417  intsaluni  40865  salgencntex  40879