| 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 482 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
| 2 | 1 | ssopab2i 5555 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
| 3 | df-xp 5691 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
| 4 | 2, 3 | sseqtrri 4033 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∈ wcel 2108 ⊆ wss 3951 {copab 5205 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ss 3968 df-opab 5206 df-xp 5691 |
| This theorem is referenced by: brab2a 5779 dmoprabss 7537 ecopovsym 8859 ecopovtrn 8860 ecopover 8861 enqex 10962 lterpq 11010 ltrelpr 11038 enrex 11107 ltrelsr 11108 ltrelre 11174 ltrelxr 11322 rlimpm 15536 dvdszrcl 16295 prdsle 17507 prdsless 17508 sectfval 17795 sectss 17796 ltbval 22061 opsrle 22065 lmfval 23240 isphtpc 25026 bcthlem1 25358 bcthlem5 25362 lgsquadlem1 27424 lgsquadlem2 27425 lgsquadlem3 27426 ishlg 28610 perpln1 28718 perpln2 28719 isperp 28720 iscgra 28817 isinag 28846 isleag 28855 inftmrel 33187 isinftm 33188 fldextfld1 33700 fldextfld2 33701 metidval 33889 metidss 33890 faeval 34247 filnetlem2 36380 numiunnum 36471 areacirc 37720 lcvfbr 39021 cmtfvalN 39211 cvrfval 39269 dicssdvh 41188 aks6d1c1p1rcl 42109 pellexlem3 42842 pellexlem4 42843 pellexlem5 42844 pellex 42846 rfovcnvf1od 44017 fsovrfovd 44022 |
| Copyright terms: Public domain | W3C validator |