Theorem difeq2i 4116

Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
difeq2i	⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)

Proof of Theorem difeq2i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		difeq2 4113	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)

Syntax hints:   = wceq 1533   ∖ cdif 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3420  df-dif 3948

This theorem is referenced by:  difeq12i  4117  dfun3  4265  dfin3  4266  dfin4  4267  invdif  4268  indif  4269  difundi  4279  difindi  4281  difdif2  4286  dif32  4292  difabs  4293  dfsymdif3  4296  notrab  4312  dif0  4373  unvdif  4475  difdifdir  4492  dfif3  4543  difpr  4807  iinvdif  5083  cnvin  6149  fndifnfp  7183  dif1o  8519  dfsdom2  9119  brttrcl2  9737  ttrcltr  9739  rnttrcl  9745  dju1dif  10195  m1bits  16415  clsval2  22991  mretopd  23033  cmpfi  23349  llycmpkgen2  23491  pserdvlem2  26402  nbgrssvwo2  29238  finsumvtxdg2ssteplem1  29422  frgrwopreglem3  30187  iundifdifd  32416  iundifdif  32417  difres  32454  gsumhashmul  32842  pmtrcnelor  32886  cycpmconjv  32937  cyc3conja  32952  sibfof  34047  eulerpartlemmf  34082  kur14lem2  34904  kur14lem6  34908  kur14lem7  34909  satfv1  35060  dfon4  35576  onint1  36020  bj-2upln1upl  36590  poimirlem8  37188  dfssr2  38057  prjspval2  42119  diophren  42315  ordeldif1o  42771  nonrel  43096  dssmapntrcls  43640  salincl  45792  meaiuninc  45949  carageniuncllem1  45989  iscnrm3rlem3  48089

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »