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

Theorem brco 5325
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 5321 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵)))
41, 2, 3mp2an 708 1 (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1744  wcel 2030  Vcvv 3231   class class class wbr 4685  ccom 5147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-co 5152
This theorem is referenced by:  opelco  5326  cnvco  5340  resco  5677  imaco  5678  rnco  5679  coass  5692  dffv2  6310  foeqcnvco  6595  f1eqcocnv  6596  rtrclreclem3  13844  imasleval  16248  ustuqtop4  22095  metustexhalf  22408  dftr6  31766  coep  31767  coepr  31768  dfpo2  31771  brtxp  32112  pprodss4v  32116  brpprod  32117  sscoid  32145  elfuns  32147  brimg  32169  brapply  32170  brcup  32171  brcap  32172  brsuccf  32173  funpartlem  32174  brrestrict  32181  dfrecs2  32182  dfrdg4  32183  cnvssco  38229
  Copyright terms: Public domain W3C validator