Theorem brdif 5158

Description: The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)

Assertion

Ref	Expression
brdif	⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

Proof of Theorem brdif

Step	Hyp	Ref	Expression
1		eldif 3909	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∖ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5104	. 2 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∖ 𝑆))
3		df-br 5104	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5104	. . . 4 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	4	notbii 323	. . 3 ⊢ (¬ 𝐴𝑆𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
6	3, 5	anbi12i 640	. 2 ⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
7	1, 2, 6	3bitr4i 306	1 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3896  ⟨cop 4590   class class class wbr 5103

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-br 5104

This theorem is used by:  fundif  6587  fndmdif  7039  isocnv3  7338  brdifun  8741  dflt2  13270  pltval  18497  lenlts  28102  ltgov  29053  opeldifid  33186  qtophaus  34461  dftr6  36495  dffr5  36498  fundmpss  36511  brsset  36631  dfon3  36634  brtxpsd2  36637  dffun10  36656  elfuns  36657  dfrecs2  36694  dfrdg4  36695  dfint3  36696  brub  36698  dffr7  36700  broutsideof  36866  brvdif  39178  frege124d  44746