Theorem difeq12i 4083

Description: Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)

Hypotheses

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵
difeq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
difeq12i	⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)

Proof of Theorem difeq12i

Step	Hyp	Ref	Expression
1		difeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	difeq1i 4081	. 2 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
3		difeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	difeq2i 4082	. 2 ⊢ (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷)
5	2, 4	eqtri 2752	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)

Syntax hints:   = wceq 1540   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-dif 3914

This theorem is referenced by:  indifdir  4254  difrab  4277  resdifdi  6197  resdifdir  6198  preddif  6290  infdju1  10119  uniioombllem4  25463  new0  27762  clwwlknclwwlkdif  29881  gtiso  32597  satffunlem2lem2  35366  mthmpps  35542  zrdivrng  37920  isdrngo1  37923  pwfi2f1o  43058  salexct2  46310  dfnelbr2  47247