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

Theorem opelopabt 4977
Description: Closed theorem form of opelopab 4987. (Contributed by NM, 19-Feb-2013.)
Assertion
Ref Expression
opelopabt ((∀𝑥𝑦(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝑦(𝑦 = 𝐵 → (𝜓𝜒)) ∧ (𝐴𝑉𝐵𝑊)) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜒,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem opelopabt
StepHypRef Expression
1 elopab 4973 . 2 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
2 19.26-2 1797 . . . 4 (∀𝑥𝑦((𝑥 = 𝐴 → (𝜑𝜓)) ∧ (𝑦 = 𝐵 → (𝜓𝜒))) ↔ (∀𝑥𝑦(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝑦(𝑦 = 𝐵 → (𝜓𝜒))))
3 prth 594 . . . . . 6 (((𝑥 = 𝐴 → (𝜑𝜓)) ∧ (𝑦 = 𝐵 → (𝜓𝜒))) → ((𝑥 = 𝐴𝑦 = 𝐵) → ((𝜑𝜓) ∧ (𝜓𝜒))))
4 bitr 744 . . . . . 6 (((𝜑𝜓) ∧ (𝜓𝜒)) → (𝜑𝜒))
53, 4syl6 35 . . . . 5 (((𝑥 = 𝐴 → (𝜑𝜓)) ∧ (𝑦 = 𝐵 → (𝜓𝜒))) → ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜒)))
652alimi 1738 . . . 4 (∀𝑥𝑦((𝑥 = 𝐴 → (𝜑𝜓)) ∧ (𝑦 = 𝐵 → (𝜓𝜒))) → ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜒)))
72, 6sylbir 225 . . 3 ((∀𝑥𝑦(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝑦(𝑦 = 𝐵 → (𝜓𝜒))) → ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜒)))
8 copsex2t 4947 . . 3 ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜒)) ∧ (𝐴𝑉𝐵𝑊)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜒))
97, 8stoic3 1699 . 2 ((∀𝑥𝑦(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝑦(𝑦 = 𝐵 → (𝜓𝜒)) ∧ (𝐴𝑉𝐵𝑊)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜒))
101, 9syl5bb 272 1 ((∀𝑥𝑦(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝑦(𝑦 = 𝐵 → (𝜓𝜒)) ∧ (𝐴𝑉𝐵𝑊)) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1479   = wceq 1481  wex 1702  wcel 1988  cop 4174  {copab 4703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-opab 4704
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator