Theorem brcog 5830

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 5110	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦𝐷𝑥 ↔ 𝐴𝐷𝑥))
2		breq2 5111	. . . 4 ⊢ (𝑧 = 𝐵 → (𝑥𝐶𝑧 ↔ 𝑥𝐶𝐵))
3	1, 2	bi2anan9 638	. . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → ((𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧) ↔ (𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
4	3	exbidv 1921	. 2 ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → (∃𝑥(𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
5		df-co 5647	. 2 ⊢ (𝐶 ∘ 𝐷) = {⟨𝑦, 𝑧⟩ ∣ ∃𝑥(𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧)}
6	4, 5	brabga 5494	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   class class class wbr 5107   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  opelco2g  5831  brcogw  5832  brco  5834  brcodir  6092  predtrss  6295  brtpos2  8211  ertr  8686  relexpindlem  15029  znleval  21464  fcoinvbr  32534  opelco3  35762  brxrn  38356  eqvreltr  38598  frege124d  43750  funressnfv  47044  dfatcolem  47256