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

Theorem opabssxp 4762
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 4292 . 2  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
3 df-xp 4695 . 2  |-  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
42, 3sseqtr4i 3211 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 1684    C_ wss 3152   {copab 4076    X. cxp 4687
This theorem is referenced by:  brab2ga  4763  dmoprabss  5929  ecopovsym  6760  ecopovtrn  6761  ecopover  6762  enqex  8546  lterpq  8594  ltrelpr  8622  enrex  8692  ltrelsr  8693  ltrelre  8756  ltrelxr  8886  rlimpm  11974  dvdszrcl  12536  prdsle  13361  prdsless  13362  sectfval  13654  sectss  13655  ltbval  16213  opsrle  16217  lmfval  16962  isphtpc  18492  bcthlem1  18746  bcthlem5  18750  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  cmppar  25973  filnetlem2  26328  pellexlem3  26916  pellexlem4  26917  pellexlem5  26918  pellex  26920  lcvfbr  29210  cmtfvalN  29400  cvrfval  29458  dicssdvh  31376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator