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

Theorem brabga 4456
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 4200 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 brabga.2 . . . 4  |-  R  =  { <. x ,  y
>.  |  ph }
32eleq2i 2494 . . 3  |-  ( <. A ,  B >.  e.  R  <->  <. A ,  B >.  e.  { <. x ,  y >.  |  ph } )
41, 3bitri 241 . 2  |-  ( A R B  <->  <. A ,  B >.  e.  { <. x ,  y >.  |  ph } )
5 opelopabga.1 . . 3  |-  ( ( x  =  A  /\  y  =  B )  ->  ( ph  <->  ps )
)
65opelopabga 4455 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( <. A ,  B >.  e.  { <. x ,  y >.  |  ph } 
<->  ps ) )
74, 6syl5bb 249 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A R B  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   <.cop 3804   class class class wbr 4199   {copab 4252
This theorem is referenced by:  braba  4459  brabg  4461  epelg  4482  brcog  5025  fmptco  5887  ofrfval  6299  wemaplem1  7499  oemapval  7623  wemapwe  7638  fpwwe2lem2  8491  fpwwelem  8504  clim  12271  rlim  12272  vdwmc  13329  isstruct2  13461  brssc  13997  isfunc  14044  isfull  14090  isfth  14094  ipole  14567  eqgval  14972  frgpuplem  15387  dvdsr  15734  ulmval  20279  isuhgra  21321  isumgra  21333  isuslgra  21355  isusgra  21356  isausgra  21362  iscusgra  21448  iswlkon  21514  istrlon  21524  ispthon  21559  isspthon  21566  isconngra  21642  isconngra1  21643  iseupa  21670  hlimi  22673  fmptcof2  24059  isinftm  24234  metidv  24270  brae  24575  braew  24576  brfae  24582  islindf  27192
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-br 4200  df-opab 4254
  Copyright terms: Public domain W3C validator