Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opelxp1 | Structured version Visualization version GIF version |
Description: The first member of an ordered pair of classes in a Cartesian product belongs to first Cartesian product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opelxp1 | ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxp 5572 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
2 | 1 | simplbi 501 | 1 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) → 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 〈cop 4533 × cxp 5534 |
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 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-opab 5102 df-xp 5542 |
This theorem is referenced by: otelxp1 5579 dff3 6897 ressnop0 6946 swoord1 8400 swoord2 8401 isfin4p1 9894 canthp1lem2 10232 ciclcl 17261 txcmplem1 22492 txlm 22499 dvbsss 24753 nvvcop 28629 nvvop 28644 fldextfld1 31392 prsdm 31532 linedegen 34131 bj-opelresdm 35000 bj-idres 35015 opelopab3 35561 |
Copyright terms: Public domain | W3C validator |