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

Theorem brabga 4756
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 4435 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2575 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 259 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 4755 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6syl5bb 267 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wa 378   = wceq 1468  wcel 1937  cop 4001   class class class wbr 4434  {copab 4492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-br 4435  df-opab 4494
This theorem is referenced by:  braba  4759  brabg  4761  epelg  4792  brcog  5048  fmptco  6124  ofrfval  6615  isfsupp  7972  wemaplem1  8144  oemapval  8273  wemapwe  8287  fpwwe2lem2  9142  fpwwelem  9155  clim  13718  rlim  13719  vdwmc  15090  isstruct2  15291  brssc  15885  isfunc  15935  isfull  15981  isfth  15985  ipole  16569  eqgval  17026  frgpuplem  17583  dvdsr  18034  islindf  19528  ulmval  23496  hpgbr  24963  isuhgra  25186  isushgra  25189  isumgra  25203  isuslgra  25231  isusgra  25232  isausgra  25242  iscusgra  25345  iswlkon  25423  istrlon  25432  ispthon  25467  isspthon  25474  isconngra  25561  isconngra1  25562  erclwwlkeq  25700  erclwwlkneq  25712  iseupa  25853  hlimi  27004  isinftm  28653  metidv  28850  ismntoplly  28984  brae  29218  braew  29219  brfae  29225  climf  38106  isausgr  39794  issubgr  39895  isrgr  40159  isrusgr  40161  istrlson  40314  upgrwlkdvspth  40345  ispthson  40348  isspthson  40349  erclwwlkseq  40639  erclwwlksneq  40651  iscllaw  41015  iscomlaw  41016  isasslaw  41018  islininds  41429  lindepsnlininds  41435
  Copyright terms: Public domain W3C validator