Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  difrab2 Structured version   Visualization version   GIF version

Theorem difrab2 29901
 Description: Difference of two restricted class abstractions. Compare with difrab 4126. (Contributed by Thierry Arnoux, 3-Jan-2022.)
Assertion
Ref Expression
difrab2 ({𝑥𝐴𝜑} ∖ {𝑥𝐵𝜑}) = {𝑥 ∈ (𝐴𝐵) ∣ 𝜑}

Proof of Theorem difrab2
StepHypRef Expression
1 nfrab1 3308 . . 3 𝑥{𝑥𝐴𝜑}
2 nfrab1 3308 . . 3 𝑥{𝑥𝐵𝜑}
31, 2nfdif 3953 . 2 𝑥({𝑥𝐴𝜑} ∖ {𝑥𝐵𝜑})
4 nfrab1 3308 . 2 𝑥{𝑥 ∈ (𝐴𝐵) ∣ 𝜑}
5 eldif 3801 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
65anbi1i 617 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝜑))
7 andi 993 . . . . . . 7 ((𝜑 ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)) ↔ ((𝜑 ∧ ¬ 𝑥𝐵) ∨ (𝜑 ∧ ¬ 𝜑)))
8 pm3.24 393 . . . . . . . 8 ¬ (𝜑 ∧ ¬ 𝜑)
98biorfi 925 . . . . . . 7 ((𝜑 ∧ ¬ 𝑥𝐵) ↔ ((𝜑 ∧ ¬ 𝑥𝐵) ∨ (𝜑 ∧ ¬ 𝜑)))
10 ancom 454 . . . . . . 7 ((𝜑 ∧ ¬ 𝑥𝐵) ↔ (¬ 𝑥𝐵𝜑))
117, 9, 103bitr2i 291 . . . . . 6 ((𝜑 ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)) ↔ (¬ 𝑥𝐵𝜑))
1211anbi2i 616 . . . . 5 ((𝑥𝐴 ∧ (𝜑 ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑))) ↔ (𝑥𝐴 ∧ (¬ 𝑥𝐵𝜑)))
13 anass 462 . . . . 5 (((𝑥𝐴𝜑) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)) ↔ (𝑥𝐴 ∧ (𝜑 ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑))))
14 anass 462 . . . . 5 (((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝜑) ↔ (𝑥𝐴 ∧ (¬ 𝑥𝐵𝜑)))
1512, 13, 143bitr4i 295 . . . 4 (((𝑥𝐴𝜑) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)) ↔ ((𝑥𝐴 ∧ ¬ 𝑥𝐵) ∧ 𝜑))
166, 15bitr4i 270 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)))
17 rabid 3301 . . 3 (𝑥 ∈ {𝑥 ∈ (𝐴𝐵) ∣ 𝜑} ↔ (𝑥 ∈ (𝐴𝐵) ∧ 𝜑))
18 eldif 3801 . . . 4 (𝑥 ∈ ({𝑥𝐴𝜑} ∖ {𝑥𝐵𝜑}) ↔ (𝑥 ∈ {𝑥𝐴𝜑} ∧ ¬ 𝑥 ∈ {𝑥𝐵𝜑}))
19 rabid 3301 . . . . 5 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
20 rabid 3301 . . . . . . 7 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
2120notbii 312 . . . . . 6 𝑥 ∈ {𝑥𝐵𝜑} ↔ ¬ (𝑥𝐵𝜑))
22 ianor 967 . . . . . 6 (¬ (𝑥𝐵𝜑) ↔ (¬ 𝑥𝐵 ∨ ¬ 𝜑))
2321, 22bitri 267 . . . . 5 𝑥 ∈ {𝑥𝐵𝜑} ↔ (¬ 𝑥𝐵 ∨ ¬ 𝜑))
2419, 23anbi12i 620 . . . 4 ((𝑥 ∈ {𝑥𝐴𝜑} ∧ ¬ 𝑥 ∈ {𝑥𝐵𝜑}) ↔ ((𝑥𝐴𝜑) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)))
2518, 24bitri 267 . . 3 (𝑥 ∈ ({𝑥𝐴𝜑} ∖ {𝑥𝐵𝜑}) ↔ ((𝑥𝐴𝜑) ∧ (¬ 𝑥𝐵 ∨ ¬ 𝜑)))
2616, 17, 253bitr4ri 296 . 2 (𝑥 ∈ ({𝑥𝐴𝜑} ∖ {𝑥𝐵𝜑}) ↔ 𝑥 ∈ {𝑥 ∈ (𝐴𝐵) ∣ 𝜑})
273, 4, 26eqri 29887 1 ({𝑥𝐴𝜑} ∖ {𝑥𝐵𝜑}) = {𝑥 ∈ (𝐴𝐵) ∣ 𝜑}
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 386   ∨ wo 836   = wceq 1601   ∈ wcel 2106  {crab 3093   ∖ cdif 3788 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rab 3098  df-v 3399  df-dif 3794 This theorem is referenced by:  reprdifc  31307
 Copyright terms: Public domain W3C validator