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

Theorem opabssxp 4778
Description: An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
opabssxp  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  ( A  X.  B )
Distinct variable groups:    x, y, A    x, B, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem opabssxp
StepHypRef Expression
1 simpl 443 . . 3  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( x  e.  A  /\  y  e.  B
) )
21ssopab2i 4308 . 2  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
3 df-xp 4711 . 2  |-  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
42, 3sseqtr4i 3224 1  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  ( A  X.  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1696    C_ wss 3165   {copab 4092    X. cxp 4703
This theorem is referenced by:  brab2ga  4779  dmoprabss  5945  ecopovsym  6776  ecopovtrn  6777  ecopover  6778  enqex  8562  lterpq  8610  ltrelpr  8638  enrex  8708  ltrelsr  8709  ltrelre  8772  ltrelxr  8902  rlimpm  11990  dvdszrcl  12552  prdsle  13377  prdsless  13378  sectfval  13670  sectss  13671  ltbval  16229  opsrle  16233  lmfval  16978  isphtpc  18508  bcthlem1  18762  bcthlem5  18766  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  cmppar  26076  filnetlem2  26431  pellexlem3  27019  pellexlem4  27020  pellexlem5  27021  pellex  27023  lcvfbr  29832  cmtfvalN  30022  cvrfval  30080  dicssdvh  31998
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator