Theorem eluni2 4749

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 1842	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4748	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3111	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 304	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1761   ∈ wcel 2081  ∃wrex 3106  ∪ cuni 4745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-v 3439  df-uni 4746

This theorem is referenced by:  uni0b  4770  intssuni  4804  iuncom4  4833  inuni  5137  cnvuni  5643  chfnrn  6684  ssorduni  7356  unon  7402  limuni3  7423  onfununi  7830  oarec  8038  uniinqs  8227  fissuni  8675  finsschain  8677  r1sdom  9049  rankuni2b  9128  cflm  9518  coflim  9529  axdc3lem2  9719  fpwwe2lem12  9909  uniwun  10008  tskr1om2  10036  tskuni  10051  axgroth3  10099  inaprc  10104  tskmval  10107  tskmcl  10109  suplem1pr  10320  lbsextlem2  19621  lbsextlem3  19622  isbasis3g  21241  eltg2b  21251  tgcl  21261  ppttop  21299  epttop  21301  neiptoptop  21423  tgcmp  21693  locfincmp  21818  dissnref  21820  comppfsc  21824  1stckgenlem  21845  txuni2  21857  txcmplem1  21933  tgqtop  22004  filuni  22177  alexsubALTlem4  22342  ptcmplem3  22346  ptcmplem4  22347  utoptop  22526  icccmplem1  23113  icccmplem3  23115  cnheibor  23242  bndth  23245  lebnumlem1  23248  bcthlem4  23613  ovolicc2lem5  23805  dyadmbllem  23883  itg2gt0  24044  rexunirn  29948  unipreima  30081  acunirnmpt2  30095  acunirnmpt2f  30096  reff  30720  locfinreflem  30721  cmpcref  30731  ddemeas  31112  dya2iocuni  31158  bnj1379  31719  cvmsss2  32130  cvmseu  32132  untuni  32544  dfon2lem3  32639  dfon2lem7  32643  dfon2lem8  32644  frrlem9  32741  brbigcup  32969  neibastop1  33317  neibastop2lem  33318  fvineqsneq  34243  heicant  34477  mblfinlem1  34479  cover2  34540  heiborlem9  34648  unichnidl  34860  erim2  35461  prtlem16  35555  prter2  35567  prter3  35568  restuni3  40943  disjinfi  41013  cncfuni  41730  intsaluni  42174  salgencntex  42188