Theorem brco 5214

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

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  Vcvv 3173   class class class wbr 4583   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  opelco  5215  cnvco  5230  resco  5556  imaco  5557  rnco  5558  coass  5571  dffv2  6181  foeqcnvco  6455  f1eqcocnv  6456  rtrclreclem3  13648  imasleval  16024  ustuqtop4  21858  metustexhalf  22171  dftr6  30893  coep  30894  coepr  30895  dfpo2  30898  brtxp  31157  pprodss4v  31161  brpprod  31162  sscoid  31190  elfuns  31192  brimg  31214  brapply  31215  brcup  31216  brcap  31217  brsuccf  31218  funpartlem  31219  brrestrict  31226  dfrecs2  31227  dfrdg4  31228  cnvssco  36931