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

Theorem brabga 4750
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 4440 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 brabga.2 . . . 4  |-  R  =  { <. x ,  y
>.  |  ph }
32eleq2i 2532 . . 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 4749 . 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 367    = wceq 1398    e. wcel 1823   <.cop 4022   class class class wbr 4439   {copab 4496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498
This theorem is referenced by:  braba  4753  brabg  4755  epelg  4781  brcog  5158  fmptco  6040  ofrfval  6521  isfsupp  7825  wemaplem1  7963  oemapval  8093  wemapwe  8130  wemapweOLD  8131  fpwwe2lem2  8999  fpwwelem  9012  clim  13399  rlim  13400  vdwmc  14580  isstruct2  14725  brssc  15302  isfunc  15352  isfull  15398  isfth  15402  ipole  15987  eqgval  16449  frgpuplem  16989  dvdsr  17490  islindf  19014  ulmval  22941  hpgbr  24330  isuhgra  24500  isushgra  24503  isumgra  24517  isuslgra  24545  isusgra  24546  isausgra  24556  iscusgra  24658  iswlkon  24736  istrlon  24745  ispthon  24780  isspthon  24787  isconngra  24874  isconngra1  24875  erclwwlkeq  25013  erclwwlkneq  25025  iseupa  25167  hlimi  26303  isinftm  27959  metidv  28106  ismntoplly  28237  brae  28450  braew  28451  brfae  28457  climf  31867  isfusgra  32796  iscllaw  32885  iscomlaw  32886  isasslaw  32888  islininds  33301  lindepsnlininds  33307
  Copyright terms: Public domain W3C validator