Theorem difeq12i 4060

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

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4046

This theorem is used by:  indifdir  4239  difrab  4262  resdifdi  6240  resdifdir  6241  preddif  6335  infdju1  10275  uniioombllem4  25916  new0  28259  clwwlknclwwlkdif  30579  gtiso  33345  satffunlem2lem2  36289  mthmpps  36465  zrdivrng  39024  isdrngo1  39027  pwfi2f1o  44235  salexct2  47485  dfnelbr2  48479