![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opabssxp | Structured version Visualization version GIF version |
Description: An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
opabssxp | ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 481 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | 1 | ssopab2i 5555 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
3 | df-xp 5687 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
4 | 2, 3 | sseqtrri 4016 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 ∈ wcel 2098 ⊆ wss 3946 {copab 5214 × cxp 5679 |
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-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-ss 3963 df-opab 5215 df-xp 5687 |
This theorem is referenced by: brab2a 5774 dmoprabss 7527 ecopovsym 8847 ecopovtrn 8848 ecopover 8849 enqex 10961 lterpq 11009 ltrelpr 11037 enrex 11106 ltrelsr 11107 ltrelre 11173 ltrelxr 11321 rlimpm 15497 dvdszrcl 16256 prdsle 17472 prdsless 17473 sectfval 17762 sectss 17763 ltbval 22042 opsrle 22046 lmfval 23219 isphtpc 25003 bcthlem1 25335 bcthlem5 25339 lgsquadlem1 27401 lgsquadlem2 27402 lgsquadlem3 27403 ishlg 28521 perpln1 28629 perpln2 28630 isperp 28631 iscgra 28728 isinag 28757 isleag 28766 inftmrel 33022 isinftm 33023 fldextfld1 33510 fldextfld2 33511 metidval 33661 metidss 33662 faeval 34035 filnetlem2 36039 areacirc 37362 lcvfbr 38666 cmtfvalN 38856 cvrfval 38914 dicssdvh 40833 aks6d1c1p1rcl 41754 pellexlem3 42425 pellexlem4 42426 pellexlem5 42427 pellex 42429 rfovcnvf1od 43608 fsovrfovd 43613 |
Copyright terms: Public domain | W3C validator |