Theorem difeq12i 4079

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 4077	. 2 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)
3		difeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	difeq2i 4078	. 2 ⊢ (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷)
5	2, 4	eqtri 2788	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-dif 3909

This theorem is used by:  indifdir  4248  difrab  4271  resdifdi  6239  resdifdir  6240  preddif  6334  infdju1  10189  uniioombllem4  25798  new0  28110  clwwlknclwwlkdif  30399  gtiso  33119  satffunlem2lem2  35937  mthmpps  36113  zrdivrng  38664  isdrngo1  38667  pwfi2f1o  43883  salexct2  47113  dfnelbr2  48070