Theorem difexg 5271

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 4085	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5265	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3437   ∖ cdif 3895   ⊆ wss 3898

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905  df-ss 3915

This theorem is referenced by:  difexi  5272  difexd  5273  difex2  7702  elpwun  7711  2oconcl  8427  fnoe  8434  difsnen  8983  fodomr  9052  domss2  9060  domssex2  9061  domssex  9062  limenpsi  9076  dif1enlem  9080  sucdom2  9123  brwdom2  9470  infeq5i  9537  infdifsn  9558  dfac8clem  9934  ssfin4  10212  isf34lem1  10274  compssiso  10276  fin1a2lem7  10308  fin1a2lem13  10314  fpwwe2lem12  10544  hashgt23el  14338  pmtrfv  19372  isirred  20346  isdrng2  20667  drngmclOLD  20675  drngid2  20676  isdrngd  20689  isdrngdOLD  20691  subdrgint  20727  cnmsubglem  21376  islindf4  21784  smadiadetlem1a  22598  basdif0  22888  tgdif0  22927  clsval2  22985  cmpcld  23337  ptcmplem2  23988  iunmbl  25501  logbfval  26747  nbfusgrlevtxm2  29377  vtxdginducedm1  29543  frgrwopreglem1  30313  eigvecval  31897  elpwdifcl  32527  disjdifprg  32576  mptiffisupp  32698  padct  32725  resf1o  32737  xrge00  33024  xrge0tsmsd  33083  tocycf  33127  ist0cld  33918  locfinref  33926  ldsysgenld  34245  sigapildsys  34247  carsgclctun  34406  sitgclg  34427  ballotlemfrc  34612  ballotlem8  34622  bnj852  35005  bnj865  35007  subfacp1lem5  35300  iscvm  35375  cvmsval  35382  mdvval  35620  topdifinffinlem  37464  pibt2  37534  poimirlem15  37748  voliunnfl  37777  fdc  37858  isdrngo2  38071  lzenom  42927  diophin  42929  diophren  42970  deg1mhm  43357  stoweidlem57  46217  fourierdlem102  46368  fourierdlem114  46380  pwsal  46475  gsumge0cl  46531  caragendifcl  46674  carageniuncllem1  46681  isomenndlem  46690  hoidmv1lelem2  46752  lincdifsn  48586  lindslinindsimp1  48619  lindslinindimp2lem2  48621  lindslinindimp2lem4  48623  lindslinindsimp2lem5  48624  lindslinindsimp2  48625  lincresunit1  48639  lincresunit2  48640  lincresunit3lem2  48642  lincresunit3  48643