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

Theorem brabga 4429
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 4173 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
2 brabga.2 . . . 4  |-  R  =  { <. x ,  y
>.  |  ph }
32eleq2i 2468 . . 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 4428 . 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 1649    e. wcel 1721   <.cop 3777   class class class wbr 4172   {copab 4225
This theorem is referenced by:  braba  4432  brabg  4434  epelg  4455  brcog  4998  fmptco  5860  ofrfval  6272  wemaplem1  7471  oemapval  7595  wemapwe  7610  fpwwe2lem2  8463  fpwwelem  8476  clim  12243  rlim  12244  vdwmc  13301  isstruct2  13433  brssc  13969  isfunc  14016  isfull  14062  isfth  14066  ipole  14539  eqgval  14944  frgpuplem  15359  dvdsr  15706  ulmval  20249  isuhgra  21291  isumgra  21303  isuslgra  21325  isusgra  21326  isausgra  21332  iscusgra  21418  iswlkon  21484  istrlon  21494  ispthon  21529  isspthon  21536  isconngra  21612  isconngra1  21613  iseupa  21640  hlimi  22643  fmptcof2  24029  isinftm  24204  metidv  24240  brae  24545  braew  24546  brfae  24552  islindf  27150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227
  Copyright terms: Public domain W3C validator