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

Theorem opabssxp 5729
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 484 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5512 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5644 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtrri 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