Theorem brco 5799

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 5795	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
4	1, 2, 3	mp2an 689	1 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1780   ∈ wcel 2105  Vcvv 3441   class class class wbr 5087   ∘ ccom 5611

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-br 5088  df-opab 5150  df-co 5616

This theorem is referenced by:  opelco  5800  cnvco  5814  cotrg  6034  cotrgOLD  6035  resco  6175  imaco  6176  rnco  6177  coass  6190  dfpo2  6221  dffv2  6902  foeqcnvco  7211  f1eqcocnv  7212  f1eqcocnvOLD  7213  ttrclss  9549  rtrclreclem3  14843  imasleval  17322  ustuqtop4  23468  metustexhalf  23784  dftr6  33818  coep  33819  coepr  33820  brtxp  34240  pprodss4v  34244  brpprod  34245  sscoid  34273  elfuns  34275  brimg  34297  brapply  34298  brcup  34299  brcap  34300  brsuccf  34301  funpartlem  34302  brrestrict  34309  dfrecs2  34310  dfrdg4  34311  cnvssco  41435