Theorem difeq1 3683

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
difeq1	⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Proof of Theorem difeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabeq 3166	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶})
2		dfdif2 3549	. 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶}
3		dfdif2 3549	. 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}
4	1, 2, 3	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977  {crab 2900   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-dif 3543

This theorem is referenced by:  difeq12  3685  difeq1i  3686  difeq1d  3689  symdifeq1  3808  uneqdifeq  4009  uneqdifeqOLD  4010  hartogslem1  8330  kmlem9  8863  kmlem11  8865  kmlem12  8866  isfin1a  8997  fin1a2lem13  9117  fundmge2nop0  13129  incexclem  14407  coprmprod  15213  coprmproddvds  15215  ismri  16114  f1otrspeq  17690  pmtrval  17694  pmtrfrn  17701  symgsssg  17710  symgfisg  17711  symggen  17713  psgnunilem1  17736  psgnunilem5  17737  psgneldm  17746  ablfac1eulem  18294  islbs  18897  lbsextlem1  18979  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  zrhcofipsgn  19758  submafval  20204  m1detdiag  20222  lpval  20753  2ndcdisj  21069  isufil  21517  ptcmplem2  21667  mblsplit  23107  voliunlem3  23127  ig1pval  23736  nb3graprlem2  25981  iscusgra  25985  isuvtx  26016  isfrgra  26517  1vwmgra  26530  3vfriswmgra  26532  difeq  28739  sigaval  29500  issiga  29501  issgon  29513  isros  29558  unelros  29561  difelros  29562  inelsros  29568  diffiunisros  29569  rossros  29570  inelcarsg  29700  carsgclctunlem2  29708  probun  29808  ballotlemgval  29912  cvmscbv  30494  cvmsi  30501  cvmsval  30502  poimirlem4  32583  sdrgacs  36790  dssmapfvd  37331  compne  37665  dvmptfprod  38835  caragensplit  39390  vonvolmbllem  39550  vonvolmbl  39551  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  nbgr0vtx  40578  nb3grprlem2  40609  uvtxa01vtx0  40623  cplgr1v  40652  dfconngr1  41355  isconngr1  41357  isfrgr  41430  frgr1v  41441  nfrgr2v  41442  frgr3v  41445  1vwmgr  41446  3vfriswmgr  41448  ldepsnlinc  42091