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

Theorem opabssxp 5079
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:   , ,   , ,

Proof of Theorem opabssxp
StepHypRef Expression
1 simpl 457 . . 3
21ssopab2i 4780 . 2
3 df-xp 5010 . 2
42, 3sseqtr4i 3536 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  e.wcel 1818  C_wss 3475  {copab 4509  X.cxp 5002
This theorem is referenced by:  brab2ga  5080  dmoprabss  6384  ecopovsym  7432  ecopovtrn  7433  ecopover  7434  enqex  9321  lterpq  9369  ltrelpr  9397  enrex  9465  ltrelsr  9466  ltrelre  9532  ltrelxr  9669  rlimpm  13323  dvdszrcl  13991  prdsle  14859  prdsless  14860  sectfval  15146  sectss  15147  ltbval  18136  opsrle  18140  lmfval  19733  isphtpc  21494  bcthlem1  21763  bcthlem5  21767  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  ishlg  23986  perpln1  24087  perpln2  24088  isperp  24089  iscgra  24169  inftmrel  27724  isinftm  27725  metidval  27869  metidss  27870  faeval  28218  filnetlem2  30197  pellexlem3  30767  pellexlem4  30768  pellexlem5  30769  pellex  30771  lcvfbr  34745  cmtfvalN  34935  cvrfval  34993  dicssdvh  36913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator