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

Theorem brabga 5539
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 5144 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2833 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 275 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 5538 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6bitrid 283 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  cop 4632   class class class wbr 5143  {copab 5205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206
This theorem is referenced by:  braba  5542  brabg  5544  epelg  5585  brcog  5877  fmptco  7149  ofrfvalg  7705  isfsupp  9405  wemaplem1  9586  oemapval  9723  wemapwe  9737  fpwwe2lem2  10672  fpwwelem  10685  clim  15530  rlim  15531  vdwmc  17016  isstruct2  17186  brssc  17858  isfunc  17909  isfull  17957  isfth  17961  ipole  18579  eqgval  19195  frgpuplem  19790  dvdsr  20362  islindf  21832  ulmval  26423  hpgbr  28768  isausgr  29181  issubgr  29288  isrgr  29577  isrusgr  29579  istrlson  29725  upgrwlkdvspth  29759  ispthson  29762  isspthson  29763  erclwwlkeq  30037  erclwwlkneq  30086  hlimi  31207  isinftm  33188  brfldext  33698  brfinext  33704  fldext2chn  33769  constrextdg2lem  33789  metidv  33891  ismntoplly  34026  brae  34242  braew  34243  brfae  34249  satfbrsuc  35371  prv  35433  bj-epelg  37069  bj-ideqgALT  37159  bj-idreseq  37163  bj-idreseqb  37164  bj-ideqg1ALT  37166  brcoss  38432  brcoels  38436  brdmqss  38647  aks6d1c1p1  42108  climf  45637  climf2  45681  nelbr  47286  iscllaw  48105  iscomlaw  48106  isasslaw  48108  islininds  48363  lindepsnlininds  48369
  Copyright terms: Public domain W3C validator