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 483 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | 1 | ssopab2i 5428 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
3 | df-xp 5554 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
4 | 2, 3 | sseqtrri 4001 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∈ wcel 2105 ⊆ wss 3933 {copab 5119 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-in 3940 df-ss 3949 df-opab 5120 df-xp 5554 |
This theorem is referenced by: brab2a 5637 dmoprabss 7245 ecopovsym 8388 ecopovtrn 8389 ecopover 8390 enqex 10332 lterpq 10380 ltrelpr 10408 enrex 10477 ltrelsr 10478 ltrelre 10544 ltrelxr 10690 rlimpm 14845 dvdszrcl 15600 prdsle 16723 prdsless 16724 sectfval 17009 sectss 17010 ltbval 20180 opsrle 20184 lmfval 21768 isphtpc 23525 bcthlem1 23854 bcthlem5 23858 lgsquadlem1 25883 lgsquadlem2 25884 lgsquadlem3 25885 ishlg 26315 perpln1 26423 perpln2 26424 isperp 26425 iscgra 26522 isinag 26551 isleag 26560 inftmrel 30736 isinftm 30737 fldextfld1 30938 fldextfld2 30939 metidval 31029 metidss 31030 faeval 31404 filnetlem2 33624 areacirc 34868 lcvfbr 36036 cmtfvalN 36226 cvrfval 36284 dicssdvh 38202 pellexlem3 39306 pellexlem4 39307 pellexlem5 39308 pellex 39310 rfovcnvf1od 40228 fsovrfovd 40233 |
Copyright terms: Public domain | W3C validator |