Theorem eluni2 4367

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 1773	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4366	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 2898	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 290	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 194   ∧ wa 382  ∃wex 1694   ∈ wcel 1976  ∃wrex 2893  ∪ cuni 4363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-v 3171  df-uni 4364

This theorem is referenced by:  uni0b  4390  intssuni  4425  iuncom4  4455  inuni  4745  cnvuni  5216  chfnrn  6218  ssorduni  6851  unon  6897  limuni3  6918  onfununi  7299  oarec  7503  uniinqs  7688  fissuni  8128  finsschain  8130  r1sdom  8494  rankuni2b  8573  cflm  8929  coflim  8940  axdc3lem2  9130  fpwwe2lem12  9316  uniwun  9415  tskr1om2  9443  tskuni  9458  axgroth3  9506  inaprc  9511  tskmval  9514  tskmcl  9516  suplem1pr  9727  lbsextlem2  18923  lbsextlem3  18924  isbasis3g  20503  eltg2b  20513  tgcl  20523  ppttop  20560  epttop  20562  neiptoptop  20684  tgcmp  20953  locfincmp  21078  dissnref  21080  comppfsc  21084  1stckgenlem  21105  txuni2  21117  txcmplem1  21193  tgqtop  21264  filuni  21438  alexsubALTlem4  21603  ptcmplem3  21607  ptcmplem4  21608  utoptop  21787  icccmplem1  22362  icccmplem3  22364  cnheibor  22490  bndth  22493  lebnumlem1  22496  bcthlem4  22846  ovolicc2lem5  23010  dyadmbllem  23087  itg2gt0  23247  rexunirn  28518  unipreima  28629  acunirnmpt2  28645  acunirnmpt2f  28646  reff  29037  locfinreflem  29038  cmpcref  29048  ddemeas  29429  dya2iocuni  29475  bnj1379  29958  cvmsss2  30313  cvmseu  30315  untuni  30643  dfon2lem3  30737  dfon2lem7  30741  dfon2lem8  30742  brbigcup  30978  neibastop1  31327  neibastop2lem  31328  heicant  32414  mblfinlem1  32416  cover2  32478  heiborlem9  32588  unichnidl  32800  prtlem16  32972  prter2  32984  prter3  32985  restuni3  38133  disjinfi  38175  cncfuni  38573  intsaluni  39024  salgencntex  39038