Theorem brcog 5811

Description: Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)

Assertion

Ref	Expression
brcog	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))

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

Allowed substitution hints:   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem brcog

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5078	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦𝐷𝑥 ↔ 𝐴𝐷𝑥))
2		breq2 5079	. . . 4 ⊢ (𝑧 = 𝐵 → (𝑥𝐶𝑧 ↔ 𝑥𝐶𝐵))
3	1, 2	bi2anan9 645	. . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → ((𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧) ↔ (𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
4	3	exbidv 1929	. 2 ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → (∃𝑥(𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
5		df-co 5630	. 2 ⊢ (𝐶 ∘ 𝐷) = {⟨𝑦, 𝑧⟩ ∣ ∃𝑥(𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧)}
6	4, 5	brabga 5479	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ∃wex 1787   ∈ wcel 2121   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:  opelco2g  5812  brcogw  5813  brco  5815  brcodir  6076  predtrss  6277  brtpos2  8176  ertr  8653  relexpindlem  15020  znleval  21533  fcoinvbr  32698  opelco3  36018  brxrn  38765  eqvreltr  39073  frege124d  44220  funressnfv  47520  dfatcolem  47732