| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > opelco | Structured version Visualization version GIF version | ||
| Description: Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.) |
| Ref | Expression |
|---|---|
| opelco.1 | ⊢ 𝐴 ∈ V |
| opelco.2 | ⊢ 𝐵 ∈ V |
| Ref | Expression |
|---|---|
| opelco | ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-br 5144 | . 2 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷)) | |
| 2 | opelco.1 | . . 3 ⊢ 𝐴 ∈ V | |
| 3 | opelco.2 | . . 3 ⊢ 𝐵 ∈ V | |
| 4 | 2, 3 | brco 5881 | . 2 ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
| 5 | 1, 4 | bitr3i 277 | 1 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 〈cop 4632 class class class wbr 5143 ∘ ccom 5689 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-co 5694 |
| This theorem is referenced by: dmcoss 5985 dmcosseq 5987 dmcosseqOLD 5988 cotrgOLDOLD 6129 coiun 6276 co02 6280 coi1 6282 coass 6285 fmptco 7149 dftpos4 8270 ttrcltr 9756 fmptcof2 32667 cnvco1 35759 cnvco2 35760 txpss3v 35879 dffun10 35915 xrnss3v 38373 coiun1 43665 coxp 48744 |
| Copyright terms: Public domain | W3C validator |