Theorem brco 5850

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  Vcvv 3450   class class class wbr 5103   ∘ ccom 5659

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  opelco  5851  cnvco  5869  cotrg  6105  resco  6246  imaco  6247  rnco  6248  rncoOLD  6249  coass  6262  dfpo2  6294  dffv2  6974  foeqcnvco  7302  f1eqcocnv  7303  ttrclss  9702  rtrclreclem3  15136  imasleval  17630  ustuqtop4  24473  metustexhalf  24785  dftr6  36333  coep  36334  coepr  36335  brtxp  36460  pprodss4v  36464  brpprod  36465  sscoid  36493  elfuns  36495  brimg  36517  brapply  36518  brcup  36519  brcap  36520  brsuccf  36522  funpartlem  36524  brrestrict  36531  dfrecs2  36532  dfrdg4  36533  cnvssco  44449  brpermmodel  45829  xpco2  49788