MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difopab Structured version   Visualization version   GIF version

Theorem difopab 5223
Description: The difference of two ordered-pair abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
Assertion
Ref Expression
difopab ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem difopab
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relopab 5217 . . 3 Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2 reldif 5209 . . 3 (Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} → Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}))
31, 2ax-mp 5 . 2 Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
4 relopab 5217 . 2 Rel {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}
5 sbcan 3465 . . . 4 ([𝑧 / 𝑥]([𝑤 / 𝑦]𝜑[𝑤 / 𝑦] ¬ 𝜓) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓))
6 sbcan 3465 . . . . 5 ([𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓) ↔ ([𝑤 / 𝑦]𝜑[𝑤 / 𝑦] ¬ 𝜓))
76sbcbii 3478 . . . 4 ([𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓) ↔ [𝑧 / 𝑥]([𝑤 / 𝑦]𝜑[𝑤 / 𝑦] ¬ 𝜓))
8 opelopabsb 4955 . . . . 5 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
9 vex 3193 . . . . . . 7 𝑧 ∈ V
10 sbcng 3463 . . . . . . 7 (𝑧 ∈ V → ([𝑧 / 𝑥] ¬ [𝑤 / 𝑦]𝜓 ↔ ¬ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓))
119, 10ax-mp 5 . . . . . 6 ([𝑧 / 𝑥] ¬ [𝑤 / 𝑦]𝜓 ↔ ¬ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
12 vex 3193 . . . . . . . 8 𝑤 ∈ V
13 sbcng 3463 . . . . . . . 8 (𝑤 ∈ V → ([𝑤 / 𝑦] ¬ 𝜓 ↔ ¬ [𝑤 / 𝑦]𝜓))
1412, 13ax-mp 5 . . . . . . 7 ([𝑤 / 𝑦] ¬ 𝜓 ↔ ¬ [𝑤 / 𝑦]𝜓)
1514sbcbii 3478 . . . . . 6 ([𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓[𝑧 / 𝑥] ¬ [𝑤 / 𝑦]𝜓)
16 opelopabsb 4955 . . . . . . 7 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
1716notbii 310 . . . . . 6 (¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ¬ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
1811, 15, 173bitr4ri 293 . . . . 5 (¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ [𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓)
198, 18anbi12i 732 . . . 4 ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑[𝑧 / 𝑥][𝑤 / 𝑦] ¬ 𝜓))
205, 7, 193bitr4ri 293 . . 3 ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓))
21 eldif 3570 . . 3 (⟨𝑧, 𝑤⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ¬ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}))
22 opelopabsb 4955 . . 3 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ ¬ 𝜓))
2320, 21, 223bitr4i 292 . 2 (⟨𝑧, 𝑤⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)})
243, 4, 23eqrelriiv 5185 1 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384   = wceq 1480  wcel 1987  Vcvv 3190  [wsbc 3422  cdif 3557  cop 4161  {copab 4682  Rel wrel 5089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-opab 4684  df-xp 5090  df-rel 5091
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator