Theorem eluni2 4376

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 1774	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4375	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 2902	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 291	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-uni 4373

This theorem is referenced by:  uni0b  4399  intssuni  4434  iuncom4  4464  inuni  4753  cnvuni  5231  chfnrn  6236  ssorduni  6877  unon  6923  limuni3  6944  onfununi  7325  oarec  7529  uniinqs  7714  fissuni  8154  finsschain  8156  r1sdom  8520  rankuni2b  8599  cflm  8955  coflim  8966  axdc3lem2  9156  fpwwe2lem12  9342  uniwun  9441  tskr1om2  9469  tskuni  9484  axgroth3  9532  inaprc  9537  tskmval  9540  tskmcl  9542  suplem1pr  9753  lbsextlem2  18980  lbsextlem3  18981  isbasis3g  20564  eltg2b  20574  tgcl  20584  ppttop  20621  epttop  20623  neiptoptop  20745  tgcmp  21014  locfincmp  21139  dissnref  21141  comppfsc  21145  1stckgenlem  21166  txuni2  21178  txcmplem1  21254  tgqtop  21325  filuni  21499  alexsubALTlem4  21664  ptcmplem3  21668  ptcmplem4  21669  utoptop  21848  icccmplem1  22433  icccmplem3  22435  cnheibor  22562  bndth  22565  lebnumlem1  22568  bcthlem4  22932  ovolicc2lem5  23096  dyadmbllem  23173  itg2gt0  23333  rexunirn  28715  unipreima  28826  acunirnmpt2  28842  acunirnmpt2f  28843  reff  29234  locfinreflem  29235  cmpcref  29245  ddemeas  29626  dya2iocuni  29672  bnj1379  30155  cvmsss2  30510  cvmseu  30512  untuni  30840  dfon2lem3  30934  dfon2lem7  30938  dfon2lem8  30939  brbigcup  31175  neibastop1  31524  neibastop2lem  31525  heicant  32614  mblfinlem1  32616  cover2  32678  heiborlem9  32788  unichnidl  33000  prtlem16  33172  prter2  33184  prter3  33185  restuni3  38333  disjinfi  38375  cncfuni  38772  intsaluni  39223  salgencntex  39237