Theorem difexg 5231

Description: Existence of a difference. (Contributed by NM, 26-May-1998.)

Assertion

Ref	Expression
difexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Proof of Theorem difexg

Step	Hyp	Ref	Expression
1		difss 4108	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5227	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 688	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494   ∖ cdif 3933   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952

This theorem is referenced by:  difexi  5232  difex2  7482  elpwun  7491  2oconcl  8128  fnoe  8135  ralxpmap  8460  difsnen  8599  domdifsn  8600  domunsncan  8617  fodomr  8668  domss2  8676  domssex2  8677  domssex  8678  mapdom2  8688  limenpsi  8692  sucdom2  8714  brwdom2  9037  infeq5i  9099  infdifsn  9120  dfac8clem  9458  acni  9471  infdif  9631  infpss  9639  ssfin4  9732  isf34lem1  9794  compssiso  9796  enfin1ai  9806  fin1a2lem7  9828  fin1a2lem13  9834  fpwwe2lem13  10064  fpwwe2  10065  canthp1lem1  10074  hashgt23el  13786  hashf1lem1  13814  brfi1indALT  13859  mrieqv2d  16910  mreexexlemd  16915  pmtrfv  18580  dpjidcl  19180  isirred  19449  isdrng2  19512  drngmcl  19515  drngid2  19518  isdrngd  19527  subdrgint  19582  cnmsubglem  20608  islindf4  20982  smadiadetlem1a  21272  basdif0  21561  tgdif0  21600  clsval2  21658  pnrmopn  21951  cmpcld  22010  cmpfi  22016  csdfil  22502  ufileu  22527  filufint  22528  alexsublem  22652  ptcmplem2  22661  bcth3  23934  iunmbl  24154  tdeglem4  24654  logbfval  25368  nbfusgrlevtxm2  27160  vtxdginducedm1  27325  frgrwopreglem1  28091  eigvecval  29673  elpwdifcl  30287  disjdifprg  30325  padct  30455  resf1o  30466  xrge00  30673  xrge0tsmsd  30692  tocycfv  30751  tocycf  30759  cyc3conja  30799  locfinref  31105  esummono  31313  esumpad  31314  esumpad2  31315  insiga  31396  ldsysgenld  31419  sigapildsys  31421  carsgclctun  31579  sitgclg  31600  ballotlemfrc  31784  ballotlem8  31794  bnj852  32193  bnj865  32195  subfacp1lem5  32431  iscvm  32506  cvmsval  32513  mdvval  32751  topdifinffinlem  34631  pibt2  34701  poimirlem15  34922  voliunnfl  34951  fdc  35035  isdrngo2  35251  selvval2lemn  39155  selvval2lem4  39156  selvval2lem5  39157  selvcl  39158  lzenom  39387  diophin  39389  diophren  39430  deg1mhm  39827  clcnvlem  40003  dssmapfv3d  40385  dssmapnvod  40386  ovolsplit  42293  stoweidlem57  42362  fourierdlem102  42513  fourierdlem114  42525  pwsal  42620  intsal  42633  gsumge0cl  42673  sge0ss  42714  sge0fodjrnlem  42718  iundjiunlem  42761  iundjiun  42762  meaiunlelem  42770  caragendifcl  42816  carageniuncllem1  42823  isomenndlem  42832  hoidmv1lelem2  42894  lincdifsn  44499  lindslinindsimp1  44532  lindslinindimp2lem2  44534  lindslinindimp2lem4  44536  lindslinindsimp2lem5  44537  lindslinindsimp2  44538  lincresunit1  44552  lincresunit2  44553  lincresunit3lem2  44555  lincresunit3  44556