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

Theorem brco 5871
Description: Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
opelco.1 𝐴 ∈ V
opelco.2 𝐵 ∈ V
Assertion
Ref Expression
brco (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷

Proof of Theorem brco
StepHypRef Expression
1 opelco.1 . 2 𝐴 ∈ V
2 opelco.2 . 2 𝐵 ∈ V
3 brcog 5867 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵)))
41, 2, 3mp2an 691 1 (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  Vcvv 3475   class class class wbr 5149  ccom 5681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-co 5686
This theorem is referenced by:  opelco  5872  cnvco  5886  cotrg  6109  cotrgOLD  6110  resco  6250  imaco  6251  rnco  6252  coass  6265  dfpo2  6296  dffv2  6987  foeqcnvco  7298  f1eqcocnv  7299  f1eqcocnvOLD  7300  ttrclss  9715  rtrclreclem3  15007  imasleval  17487  ustuqtop4  23749  metustexhalf  24065  dftr6  34721  coep  34722  coepr  34723  brtxp  34852  pprodss4v  34856  brpprod  34857  sscoid  34885  elfuns  34887  brimg  34909  brapply  34910  brcup  34911  brcap  34912  brsuccf  34913  funpartlem  34914  brrestrict  34921  dfrecs2  34922  dfrdg4  34923  cnvssco  42357
  Copyright terms: Public domain W3C validator