Theorem brco 5853

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

Step	Hyp	Ref	Expression
1		opelco.1	. 2 ⊢ 𝐴 ∈ V
2		opelco.2	. 2 ⊢ 𝐵 ∈ V
3		brcog 5849	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811   ∈ wcel 2146  Vcvv 3454   class class class wbr 5106   ∘ ccom 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-co 5664

This theorem is used by:  opelco  5854  cnvco  5872  cotrg  6111  resco  6258  imaco  6259  rnco  6260  rncoOLD  6261  coass  6274  dfpo2  6306  dffv2  6991  foeqcnvco  7318  f1eqcocnv  7319  ttrclss  9734  rtrclreclem3  15228  imasleval  17728  ustuqtop4  24578  metustexhalf  24890  dftr6  36646  coep  36647  coepr  36648  brtxp  36772  pprodss4v  36776  brpprod  36777  sscoid  36805  elfuns  36807  brimg  36829  brapply  36830  brcup  36831  brcap  36832  brsuccf  36834  funpartlem  36836  brrestrict  36843  dfrecs2  36844  dfrdg4  36845  cnvssco  44749  cocanss2  46064  brpermmodel  46135  xpco2  50110