Theorem difexg 5294

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-in 3906  df-ss 3916

This theorem is used by:  difexi  5295  difexd  5296  difex2  7759  elpwun  7768  2oconcl  8490  fnoe  8497  difsnen  9057  fodomr  9126  domss2  9134  domssex2  9135  domssex  9136  limenpsi  9150  dif1enlem  9154  sucdom2  9197  brwdom2  9545  infeq5i  9615  infdifsn  9636  dfac8clem  10035  ssfin4  10312  isf34lem1  10374  compssiso  10376  fin1a2lem7  10408  fin1a2lem13  10414  fpwwe2lem12  10651  hashgt23el  14489  pmtrfv  19579  isirred  20560  isdrng2  20906  drngid2  20919  isdrngd  20931  isdrngdOLD  20933  subdrgint  20969  cnmsubglem  21643  islindf4  22051  smadiadetlem1a  22885  basdif0  23178  tgdif0  23217  clsval2  23275  cmpcld  23627  ptcmplem2  24279  iunmbl  25781  logbfval  27027  nbfusgrlevtxm2  29838  vtxdginducedm1  30003  frgrwopreglem1  30792  eigvecval  32377  elpwdifcl  33001  disjdifprg  33048  mptiffisupp  33165  resf1o  33201  xrge00  33454  xrge0tsmsd  33513  tocycf  33557  ist0cld  34343  locfinref  34351  ldsysgenld  34671  sigapildsys  34673  carsgclctun  34832  sitgclg  34853  ballotlemfrc  35038  ballotlem8  35048  bnj852  35430  bnj865  35432  subfacp1lem5  35763  iscvm  35838  cvmsval  35845  mdvval  36083  ttcwf2  37144  topdifinffinlem  38101  pibt2  38171  poimirlem15  38384  voliunnfl  38413  fdc  38495  isdrngo2  38708  lzenom  43615  diophin  43617  diophren  43654  deg1mhm  44041  stoweidlem57  46885  fourierdlem102  47036  fourierdlem114  47048  pwsal  47143  gsumge0cl  47199  caragendifcl  47342  carageniuncllem1  47349  isomenndlem  47358  hoidmv1lelem2  47420  lincdifsn  49354  lindslinindsimp1  49387  lindslinindimp2lem2  49389  lindslinindimp2lem4  49391  lindslinindsimp2lem5  49392  lindslinindsimp2  49393  lincresunit1  49407  lincresunit2  49408  lincresunit3lem2  49410  lincresunit3  49411