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

Theorem brco 4889
Description: Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
opelco.1  |-  A  e. 
_V
opelco.2  |-  B  e. 
_V
Assertion
Ref Expression
brco  |-  ( A ( C  o.  D
) B  <->  E. x
( A D x  /\  x C B ) )
Distinct variable groups:    x, A    x, B    x, C    x, D

Proof of Theorem brco
StepHypRef Expression
1 opelco.1 . 2  |-  A  e. 
_V
2 opelco.2 . 2  |-  B  e. 
_V
3 brcog 4887 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A ( C  o.  D ) B  <->  E. x ( A D x  /\  x C B ) ) )
41, 2, 3mp2an 653 1  |-  ( A ( C  o.  D
) B  <->  E. x
( A D x  /\  x C B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1532    e. wcel 1701   _Vcvv 2822   class class class wbr 4060    o. ccom 4730
This theorem is referenced by:  opelco  4890  cnvco  4902  resco  5214  imaco  5215  rnco  5216  coass  5228  dffv2  5630  foeqcnvco  5846  f1eqcocnv  5847  imasleval  13492  metustexhalf  23498  rtrclreclem.trans  24327  dftr6  24492  coep  24493  coepr  24494  dfpo2  24497  brtxp  24805  pprodss4v  24809  brpprod  24810  dffun10  24838  elfuns  24839  brimg  24861  brapply  24862  brcup  24863  brcap  24864  brsuccf  24865  funpartlem  24866  brrestrict  24873  dfrdg4  24874  tfrqfree  24875
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-co 4735
  Copyright terms: Public domain W3C validator