![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brcog | Structured version Visualization version GIF version |
Description: Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.) |
Ref | Expression |
---|---|
brcog | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 5152 | . . . 4 ⊢ (𝑦 = 𝐴 → (𝑦𝐷𝑥 ↔ 𝐴𝐷𝑥)) | |
2 | breq2 5153 | . . . 4 ⊢ (𝑧 = 𝐵 → (𝑥𝐶𝑧 ↔ 𝑥𝐶𝐵)) | |
3 | 1, 2 | bi2anan9 636 | . . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → ((𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧) ↔ (𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) |
4 | 3 | exbidv 1916 | . 2 ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → (∃𝑥(𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) |
5 | df-co 5687 | . 2 ⊢ (𝐶 ∘ 𝐷) = {〈𝑦, 𝑧〉 ∣ ∃𝑥(𝑦𝐷𝑥 ∧ 𝑥𝐶𝑧)} | |
6 | 4, 5 | brabga 5536 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∃wex 1773 ∈ wcel 2098 class class class wbr 5149 ∘ ccom 5682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-co 5687 |
This theorem is referenced by: opelco2g 5870 brcogw 5871 brco 5873 brcodir 6126 predtrss 6330 brtpos2 8238 ertr 8740 relexpindlem 15046 znleval 21505 fcoinvbr 32474 opelco3 35501 brxrn 37976 eqvreltr 38209 frege124d 43333 funressnfv 46563 dfatcolem 46773 |
Copyright terms: Public domain | W3C validator |