| 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 487 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
| 2 | 1 | ssopab2i 5525 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| 3 | df-xp 5657 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
| 4 | 2, 3 | sseqtrri 3988 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 400 ∈ wcel 2145 ⊆ wss 3907 {copab 5166 × cxp 5649 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-ss 3924 df-opab 5167 df-xp 5657 |
| This theorem is referenced by: brab2a 5744 dmoprabss 7504 ecopovsym 8805 ecopovtrn 8806 ecopover 8807 enqex 10895 lterpq 10943 ltrelpr 10971 enrex 11040 ltrelsr 11041 ltrelre 11107 ltrelxr 11258 rlimpm 15539 dvdszrcl 16303 prdsle 17503 prdsless 17504 sectfval 17796 sectss 17797 ltbval 22151 opsrle 22155 lmfval 23346 isphtpc 25110 bcthlem1 25440 bcthlem5 25444 lgsquadlem1 27498 lgsquadlem2 27499 lgsquadlem3 27500 ishlg 28825 perpln1 28937 perpln2 28938 isperp 28939 iscgra 29057 isinag 29086 isleag 29095 inftmrel 33408 isinftm 33409 fldextfld1 33949 fldextfld2 33950 metidval 34192 metidss 34193 faeval 34548 filnetlem2 36747 numiunnum 36838 areacirc 38219 lcvfbr 39651 cmtfvalN 39841 cvrfval 39899 dicssdvh 41817 aks6d1c1p1rcl 42732 pellexlem3 43415 pellexlem4 43416 pellexlem5 43417 pellex 43419 rfovcnvf1od 44587 fsovrfovd 44592 sectfn 49659 |
| Copyright terms: Public domain | W3C validator |