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

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

Proof of Theorem brabga
StepHypRef Expression
1 df-br 4797 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2823 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 264 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 5130 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6syl5bb 272 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1624   ∈ wcel 2131  ⟨cop 4319   class class class wbr 4796  {copab 4856 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797  df-opab 4857 This theorem is referenced by:  braba  5134  brabg  5136  epelg  5172  brcog  5436  fmptco  6551  ofrfval  7062  isfsupp  8436  wemaplem1  8608  oemapval  8745  wemapwe  8759  fpwwe2lem2  9638  fpwwelem  9651  clim  14416  rlim  14417  vdwmc  15876  isstruct2  16061  brssc  16667  isfunc  16717  isfull  16763  isfth  16767  ipole  17351  eqgval  17836  frgpuplem  18377  dvdsr  18838  islindf  20345  ulmval  24325  hpgbr  25843  isausgr  26250  issubgr  26354  isrgr  26657  isrusgr  26659  istrlson  26805  upgrwlkdvspth  26837  ispthson  26840  isspthson  26841  erclwwlkeq  27133  erclwwlkneq  27190  hlimi  28346  isinftm  30036  metidv  30236  ismntoplly  30370  brae  30605  braew  30606  brfae  30612  brcoss  34501  brcoels  34505  climf  40349  climf2  40393  nelbr  41792  iscllaw  42327  iscomlaw  42328  isasslaw  42330  islininds  42737  lindepsnlininds  42743
 Copyright terms: Public domain W3C validator