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

Theorem opabssxp 5773
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 481 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5555 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5687 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtrri 4016 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 394  wcel 2098  wss 3946  {copab 5214   × cxp 5679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-ss 3963  df-opab 5215  df-xp 5687
This theorem is referenced by:  brab2a  5774  dmoprabss  7527  ecopovsym  8847  ecopovtrn  8848  ecopover  8849  enqex  10961  lterpq  11009  ltrelpr  11037  enrex  11106  ltrelsr  11107  ltrelre  11173  ltrelxr  11321  rlimpm  15497  dvdszrcl  16256  prdsle  17472  prdsless  17473  sectfval  17762  sectss  17763  ltbval  22042  opsrle  22046  lmfval  23219  isphtpc  25003  bcthlem1  25335  bcthlem5  25339  lgsquadlem1  27401  lgsquadlem2  27402  lgsquadlem3  27403  ishlg  28521  perpln1  28629  perpln2  28630  isperp  28631  iscgra  28728  isinag  28757  isleag  28766  inftmrel  33022  isinftm  33023  fldextfld1  33510  fldextfld2  33511  metidval  33661  metidss  33662  faeval  34035  filnetlem2  36039  areacirc  37362  lcvfbr  38666  cmtfvalN  38856  cvrfval  38914  dicssdvh  40833  aks6d1c1p1rcl  41754  pellexlem3  42425  pellexlem4  42426  pellexlem5  42427  pellex  42429  rfovcnvf1od  43608  fsovrfovd  43613
  Copyright terms: Public domain W3C validator