Theorem opelco 5816

Description: Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)

Hypotheses

Ref	Expression
opelco.1	⊢ 𝐴 ∈ V
opelco.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
opelco	⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷

Proof of Theorem opelco

Step	Hyp	Ref	Expression
1		df-br 5076	. 2 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷))
2		opelco.1	. . 3 ⊢ 𝐴 ∈ V
3		opelco.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	brco 5815	. 2 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
5	1, 4	bitr3i 279	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 397  ∃wex 1787   ∈ wcel 2121  Vcvv 3433  ⟨cop 4564   class class class wbr 5075   ∘ ccom 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-co 5630

This theorem is referenced by:  dmcoss  5924  dmcossOLD  5925  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  coiun  6212  co02  6216  coi1  6218  coass  6221  fmptco  7075  dftpos4  8189  ttrcltr  9632  fmptcof2  32753  cnvco1  36002  cnvco2  36003  txpss3v  36119  dffun10  36155  xrnss3v  38763  coiun1  44111  coxp  49337