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

Theorem brabga 4767
Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
Hypotheses
Ref Expression
opelopabga.1  |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph  <->  ps )
)
brabga.2  |-  R  =  { <. x ,  y
>.  |  ph }
Assertion
Ref Expression
brabga  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A R B  <->  ps ) )
Distinct variable groups:    x, y, A    x, B, y    ps, x, y
Allowed substitution hints:    ph( x, y)    R( x, y)    V( x, y)    W( x, y)

Proof of Theorem brabga
StepHypRef Expression
1 df-br 4454 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 brabga.2 . . . 4  |-  R  =  { <. x ,  y
>.  |  ph }
32eleq2i 2545 . . 3  |-  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  { <. x ,  y >.  |  ph } )
41, 3bitri 249 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  { <. x ,  y >.  |  ph } )
5 opelopabga.1 . . 3  |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph  <->  ps )
)
65opelopabga 4766 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( <. A ,  B >.  e.  { <. x ,  y >.  |  ph } 
<->  ps ) )
74, 6syl5bb 257 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A R B  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   <.cop 4039   class class class wbr 4453   {copab 4510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-br 4454  df-opab 4512
This theorem is referenced by:  braba  4770  brabg  4772  epelg  4798  brcog  5175  fmptco  6065  ofrfval  6543  isfsupp  7845  wemaplem1  7983  oemapval  8114  wemapwe  8151  wemapweOLD  8152  fpwwe2lem2  9022  fpwwelem  9035  clim  13297  rlim  13298  vdwmc  14372  isstruct2  14516  brssc  15061  isfunc  15108  isfull  15154  isfth  15158  ipole  15662  eqgval  16122  frgpuplem  16663  dvdsr  17167  islindf  18716  ulmval  22642  legov  23837  isuhgra  24112  isushgra  24115  isumgra  24129  isuslgra  24157  isusgra  24158  isausgra  24168  iscusgra  24270  iswlkon  24348  istrlon  24357  ispthon  24392  isspthon  24399  isconngra  24486  isconngra1  24487  erclwwlkeq  24625  erclwwlkneq  24637  iseupa  24779  hlimi  25919  fmptcof2  27316  isinftm  27540  metidv  27687  ismntoplly  27819  brae  28029  braew  28030  brfae  28036  climf  31478  isfusgra  32205  iscllaw  32260  iscomlaw  32261  isasslaw  32263  islininds  32484  lindepsnlininds  32490
  Copyright terms: Public domain W3C validator