Theorem brdif 5196

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 3961	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∖ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5144	. 2 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∖ 𝑆))
3		df-br 5144	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5144	. . . 4 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	4	notbii 320	. . 3 ⊢ (¬ 𝐴𝑆𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
6	3, 5	anbi12i 628	. 2 ⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
7	1, 2, 6	3bitr4i 303	1 ⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ∖ cdif 3948  ⟨cop 4632   class class class wbr 5143

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-br 5144

This theorem is referenced by:  fundif  6615  fndmdif  7062  isocnv3  7352  brdifun  8775  dflt2  13190  pltval  18377  slenlt  27797  ltgov  28605  opeldifid  32612  qtophaus  33835  dftr6  35751  dffr5  35754  fundmpss  35767  brsset  35890  dfon3  35893  brtxpsd2  35896  dffun10  35915  elfuns  35916  dfrecs2  35951  dfrdg4  35952  dfint3  35953  brub  35955  broutsideof  36122  brvdif  38262  frege124d  43774