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

Theorem opabssxp 5227
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 472 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5032 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5149 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtr4i 3671 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 2030  wss 3607  {copab 4745   × cxp 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621  df-opab 4746  df-xp 5149
This theorem is referenced by:  brab2a  5228  dmoprabss  6784  ecopovsym  7892  ecopovtrn  7893  ecopover  7894  enqex  9782  lterpq  9830  ltrelpr  9858  enrex  9926  ltrelsr  9927  ltrelre  9993  ltrelxr  10137  rlimpm  14275  dvdszrcl  15032  prdsle  16169  prdsless  16170  sectfval  16458  sectss  16459  ltbval  19519  opsrle  19523  lmfval  21084  isphtpc  22840  bcthlem1  23167  bcthlem5  23171  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  ishlg  25542  perpln1  25650  perpln2  25651  isperp  25652  iscgra  25746  isinag  25774  isleag  25778  inftmrel  29862  isinftm  29863  metidval  30061  metidss  30062  faeval  30437  filnetlem2  32499  areacirc  33635  lcvfbr  34625  cmtfvalN  34815  cvrfval  34873  dicssdvh  36792  pellexlem3  37712  pellexlem4  37713  pellexlem5  37714  pellex  37716  rfovcnvf1od  38615  fsovrfovd  38620
  Copyright terms: Public domain W3C validator