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

Theorem oprabbid 7236
Description: Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
Hypotheses
Ref Expression
oprabbid.1 𝑥𝜑
oprabbid.2 𝑦𝜑
oprabbid.3 𝑧𝜑
oprabbid.4 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
oprabbid (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)   𝜒(𝑥,𝑦,𝑧)

Proof of Theorem oprabbid
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 oprabbid.1 . . . 4 𝑥𝜑
2 oprabbid.2 . . . . 5 𝑦𝜑
3 oprabbid.3 . . . . . 6 𝑧𝜑
4 oprabbid.4 . . . . . . 7 (𝜑 → (𝜓𝜒))
54anbi2d 632 . . . . . 6 (𝜑 → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜓) ↔ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜒)))
63, 5exbid 2225 . . . . 5 (𝜑 → (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜓) ↔ ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜒)))
72, 6exbid 2225 . . . 4 (𝜑 → (∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜓) ↔ ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜒)))
81, 7exbid 2225 . . 3 (𝜑 → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜓) ↔ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜒)))
98abbidv 2803 . 2 (𝜑 → {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜓)} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜒)})
10 df-oprab 7177 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜓)}
11 df-oprab 7177 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜒)}
129, 10, 113eqtr4g 2799 1 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wex 1786  wnf 1790  {cab 2717  cop 4523  {coprab 7174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-12 2179  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-oprab 7177
This theorem is referenced by:  oprabbidv  7237  mpoeq123  7243
  Copyright terms: Public domain W3C validator