Theorem eluni2 4634

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 1947	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4633	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3102	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 294	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 197   ∧ wa 384  ∃wex 1859   ∈ wcel 2156  ∃wrex 3097  ∪ cuni 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-v 3393  df-uni 4631

This theorem is referenced by:  uni0b  4657  intssuni  4691  iuncom4  4720  inuni  5018  cnvuni  5510  chfnrn  6546  ssorduni  7211  unon  7257  limuni3  7278  onfununi  7670  oarec  7875  uniinqs  8058  fissuni  8506  finsschain  8508  r1sdom  8880  rankuni2b  8959  cflm  9353  coflim  9364  axdc3lem2  9554  fpwwe2lem12  9744  uniwun  9843  tskr1om2  9871  tskuni  9886  axgroth3  9934  inaprc  9939  tskmval  9942  tskmcl  9944  suplem1pr  10155  lbsextlem2  19364  lbsextlem3  19365  isbasis3g  20963  eltg2b  20973  tgcl  20983  ppttop  21021  epttop  21023  neiptoptop  21145  tgcmp  21414  locfincmp  21539  dissnref  21541  comppfsc  21545  1stckgenlem  21566  txuni2  21578  txcmplem1  21654  tgqtop  21725  filuni  21898  alexsubALTlem4  22063  ptcmplem3  22067  ptcmplem4  22068  utoptop  22247  icccmplem1  22834  icccmplem3  22836  cnheibor  22963  bndth  22966  lebnumlem1  22969  bcthlem4  23332  ovolicc2lem5  23498  dyadmbllem  23576  itg2gt0  23737  rexunirn  29653  unipreima  29769  acunirnmpt2  29783  acunirnmpt2f  29784  reff  30227  locfinreflem  30228  cmpcref  30238  ddemeas  30620  dya2iocuni  30666  bnj1379  31219  cvmsss2  31574  cvmseu  31576  untuni  31903  dfon2lem3  32005  dfon2lem7  32009  dfon2lem8  32010  brbigcup  32321  neibastop1  32670  neibastop2lem  32671  heicant  33752  mblfinlem1  33754  cover2  33815  heiborlem9  33924  unichnidl  34136  prtlem16  34643  prter2  34655  prter3  34656  restuni3  39787  disjinfi  39863  cncfuni  40573  intsaluni  41020  salgencntex  41034