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

Theorem opabssxp 5620
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 486 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5414 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5538 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtrri 3979 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 399  wcel 2114  wss 3908  {copab 5104   × cxp 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-v 3471  df-in 3915  df-ss 3925  df-opab 5105  df-xp 5538
This theorem is referenced by:  brab2a  5621  dmoprabss  7240  ecopovsym  8386  ecopovtrn  8387  ecopover  8388  enqex  10333  lterpq  10381  ltrelpr  10409  enrex  10478  ltrelsr  10479  ltrelre  10545  ltrelxr  10691  rlimpm  14848  dvdszrcl  15603  prdsle  16726  prdsless  16727  sectfval  17012  sectss  17013  ltbval  20709  opsrle  20713  lmfval  21835  isphtpc  23597  bcthlem1  23926  bcthlem5  23930  lgsquadlem1  25962  lgsquadlem2  25963  lgsquadlem3  25964  ishlg  26394  perpln1  26502  perpln2  26503  isperp  26504  iscgra  26601  isinag  26630  isleag  26639  inftmrel  30840  isinftm  30841  fldextfld1  31096  fldextfld2  31097  metidval  31207  metidss  31208  faeval  31579  filnetlem2  33801  areacirc  35112  lcvfbr  36278  cmtfvalN  36468  cvrfval  36526  dicssdvh  38444  pellexlem3  39706  pellexlem4  39707  pellexlem5  39708  pellex  39710  rfovcnvf1od  40640  fsovrfovd  40645
  Copyright terms: Public domain W3C validator