![]() |
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 484 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | 1 | ssopab2i 5512 | . 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} |
3 | df-xp 5644 | . 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | |
4 | 2, 3 | sseqtrri 3986 | 1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 ∈ wcel 2107 ⊆ wss 3915 {copab 5172 × cxp 5636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-opab 5173 df-xp 5644 |
This theorem is referenced by: brab2a 5730 dmoprabss 7464 ecopovsym 8765 ecopovtrn 8766 ecopover 8767 enqex 10865 lterpq 10913 ltrelpr 10941 enrex 11010 ltrelsr 11011 ltrelre 11077 ltrelxr 11223 rlimpm 15389 dvdszrcl 16148 prdsle 17351 prdsless 17352 sectfval 17641 sectss 17642 ltbval 21460 opsrle 21464 lmfval 22599 isphtpc 24373 bcthlem1 24704 bcthlem5 24708 lgsquadlem1 26744 lgsquadlem2 26745 lgsquadlem3 26746 ishlg 27586 perpln1 27694 perpln2 27695 isperp 27696 iscgra 27793 isinag 27822 isleag 27831 inftmrel 32058 isinftm 32059 fldextfld1 32378 fldextfld2 32379 metidval 32511 metidss 32512 faeval 32885 filnetlem2 34880 areacirc 36200 lcvfbr 37511 cmtfvalN 37701 cvrfval 37759 dicssdvh 39678 pellexlem3 41183 pellexlem4 41184 pellexlem5 41185 pellex 41187 rfovcnvf1od 42350 fsovrfovd 42355 |
Copyright terms: Public domain | W3C validator |