![]() |
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 476 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | 1 | ssopab2i 5240 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
3 | df-xp 5361 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
4 | 2, 3 | sseqtr4i 3856 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 386 ∈ wcel 2106 ⊆ wss 3791 {copab 4948 × cxp 5353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-in 3798 df-ss 3805 df-opab 4949 df-xp 5361 |
This theorem is referenced by: brab2a 5442 dmoprabss 7019 ecopovsym 8133 ecopovtrn 8134 ecopover 8135 enqex 10079 lterpq 10127 ltrelpr 10155 enrex 10224 ltrelsr 10225 ltrelre 10291 ltrelxr 10438 rlimpm 14639 dvdszrcl 15392 prdsle 16508 prdsless 16509 sectfval 16796 sectss 16797 ltbval 19868 opsrle 19872 lmfval 21444 isphtpc 23201 bcthlem1 23530 bcthlem5 23534 lgsquadlem1 25557 lgsquadlem2 25558 lgsquadlem3 25559 ishlg 25953 perpln1 26061 perpln2 26062 isperp 26063 iscgra 26157 isinag 26187 isleag 26196 inftmrel 30310 isinftm 30311 metidval 30545 metidss 30546 faeval 30921 filnetlem2 32976 areacirc 34124 lcvfbr 35168 cmtfvalN 35358 cvrfval 35416 dicssdvh 37334 pellexlem3 38347 pellexlem4 38348 pellexlem5 38349 pellex 38351 rfovcnvf1od 39246 fsovrfovd 39251 |
Copyright terms: Public domain | W3C validator |