MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opabssxp Structured version   Visualization version   GIF version

Theorem opabssxp 5398
Description: An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
opabssxp {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem opabssxp
StepHypRef Expression
1 simpl 475 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5199 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5318 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtr4i 3834 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 385  wcel 2157  wss 3769  {copab 4905   × cxp 5310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-in 3776  df-ss 3783  df-opab 4906  df-xp 5318
This theorem is referenced by:  brab2a  5399  dmoprabss  6976  ecopovsym  8088  ecopovtrn  8089  ecopover  8090  enqex  10032  lterpq  10080  ltrelpr  10108  enrex  10176  ltrelsr  10177  ltrelre  10243  ltrelxr  10389  rlimpm  14572  dvdszrcl  15324  prdsle  16437  prdsless  16438  sectfval  16725  sectss  16726  ltbval  19794  opsrle  19798  lmfval  21365  isphtpc  23121  bcthlem1  23450  bcthlem5  23454  lgsquadlem1  25457  lgsquadlem2  25458  lgsquadlem3  25459  ishlg  25853  perpln1  25961  perpln2  25962  isperp  25963  iscgra  26057  isinag  26085  isleag  26089  inftmrel  30250  isinftm  30251  metidval  30449  metidss  30450  faeval  30825  filnetlem2  32886  areacirc  33993  lcvfbr  35041  cmtfvalN  35231  cvrfval  35289  dicssdvh  37207  pellexlem3  38181  pellexlem4  38182  pellexlem5  38183  pellex  38185  rfovcnvf1od  39080  fsovrfovd  39085
  Copyright terms: Public domain W3C validator