| 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 5526 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| 3 | df-xp 5658 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
| 4 | 2, 3 | sseqtrri 3988 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 400 ∈ wcel 2145 ⊆ wss 3907 {copab 5167 × cxp 5650 |
| 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 5168 df-xp 5658 |
| This theorem is referenced by: brab2a 5745 dmoprabss 7504 ecopovsym 8805 ecopovtrn 8806 ecopover 8807 enqex 10895 lterpq 10943 ltrelpr 10971 enrex 11040 ltrelsr 11041 ltrelre 11107 ltrelxr 11258 rlimpm 15541 dvdszrcl 16305 prdsle 17505 prdsless 17506 sectfval 17798 sectss 17799 ltbval 22154 opsrle 22158 lmfval 23350 isphtpc 25114 bcthlem1 25444 bcthlem5 25448 lgsquadlem1 27502 lgsquadlem2 27503 lgsquadlem3 27504 ishlg 28829 perpln1 28941 perpln2 28942 isperp 28943 iscgra 29061 isinag 29090 isleag 29099 inftmrel 33413 isinftm 33414 fldextfld1 33954 fldextfld2 33955 metidval 34197 metidss 34198 faeval 34553 filnetlem2 36752 numiunnum 36843 areacirc 38224 lcvfbr 39656 cmtfvalN 39846 cvrfval 39904 dicssdvh 41822 aks6d1c1p1rcl 42737 pellexlem3 43420 pellexlem4 43421 pellexlem5 43422 pellex 43424 rfovcnvf1od 44592 fsovrfovd 44597 sectfn 49658 |
| Copyright terms: Public domain | W3C validator |