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

Theorem brabgaf 28800
 Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) (Revised by Thierry Arnoux, 17-May-2020.)
Hypotheses
Ref Expression
brabgaf.0 𝑥𝜓
brabgaf.1 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
brabgaf.2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Assertion
Ref Expression
brabgaf ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝑅(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem brabgaf
StepHypRef Expression
1 df-br 4584 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabgaf.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2680 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 263 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 elopab 4908 . . 3 (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
6 elisset 3188 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
7 elisset 3188 . . . 4 (𝐵𝑊 → ∃𝑦 𝑦 = 𝐵)
8 eeanv 2170 . . . . 5 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
9 nfe1 2014 . . . . . . 7 𝑥𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
10 brabgaf.0 . . . . . . 7 𝑥𝜓
119, 10nfbi 1821 . . . . . 6 𝑥(∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)
12 nfe1 2014 . . . . . . . . 9 𝑦𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312nfex 2140 . . . . . . . 8 𝑦𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14 nfv 1830 . . . . . . . 8 𝑦𝜓
1513, 14nfbi 1821 . . . . . . 7 𝑦(∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)
16 opeq12 4342 . . . . . . . . 9 ((𝑥 = 𝐴𝑦 = 𝐵) → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
17 copsexg 4882 . . . . . . . . . 10 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
1817eqcoms 2618 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
1916, 18syl 17 . . . . . . . 8 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20 brabgaf.1 . . . . . . . 8 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
2119, 20bitr3d 269 . . . . . . 7 ((𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
2215, 21exlimi 2073 . . . . . 6 (∃𝑦(𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
2311, 22exlimi 2073 . . . . 5 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
248, 23sylbir 224 . . . 4 ((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
256, 7, 24syl2an 493 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
265, 25syl5bb 271 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
274, 26syl5bb 271 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  ⟨cop 4131   class class class wbr 4583  {copab 4642 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644 This theorem is referenced by:  fmptcof2  28839
 Copyright terms: Public domain W3C validator