Theorem brco 5858

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  Vcvv 3457   class class class wbr 5111   ∘ ccom 5667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  opelco  5859  cnvco  5877  cotrg  6113  resco  6253  imaco  6254  rnco  6255  rncoOLD  6256  coass  6269  dfpo2  6301  dffv2  6980  foeqcnvco  7307  f1eqcocnv  7308  ttrclss  9696  rtrclreclem3  15123  imasleval  17619  ustuqtop4  24454  metustexhalf  24766  dftr6  36282  coep  36283  coepr  36284  brtxp  36409  pprodss4v  36413  brpprod  36414  sscoid  36442  elfuns  36444  brimg  36466  brapply  36467  brcup  36468  brcap  36469  brsuccf  36471  funpartlem  36473  brrestrict  36480  dfrecs2  36481  dfrdg4  36482  cnvssco  44392  brpermmodel  45772  xpco2  49694