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

Theorem brco 5717
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 5713 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵)))
41, 2, 3mp2an 690 1 (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wex 1780  wcel 2114  Vcvv 3473   class class class wbr 5042  ccom 5535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-co 5540
This theorem is referenced by:  opelco  5718  cnvco  5732  resco  6079  imaco  6080  rnco  6081  coass  6094  dffv2  6732  foeqcnvco  7033  f1eqcocnv  7034  rtrclreclem3  14399  imasleval  16793  ustuqtop4  22829  metustexhalf  23142  dftr6  32994  coep  32995  coepr  32996  dfpo2  32999  brtxp  33349  pprodss4v  33353  brpprod  33354  sscoid  33382  elfuns  33384  brimg  33406  brapply  33407  brcup  33408  brcap  33409  brsuccf  33410  funpartlem  33411  brrestrict  33418  dfrecs2  33419  dfrdg4  33420  cnvssco  40101
  Copyright terms: Public domain W3C validator