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

Theorem opabssxp 4950
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 444 . . 3  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( x  e.  A  /\  y  e.  B
) )
21ssopab2i 4482 . 2  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
3 df-xp 4884 . 2  |-  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
42, 3sseqtr4i 3381 1  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  ( A  X.  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725    C_ wss 3320   {copab 4265    X. cxp 4876
This theorem is referenced by:  brab2ga  4951  dmoprabss  6155  ecopovsym  7006  ecopovtrn  7007  ecopover  7008  enqex  8799  lterpq  8847  ltrelpr  8875  enrex  8945  ltrelsr  8946  ltrelre  9009  ltrelxr  9139  rlimpm  12294  dvdszrcl  12857  prdsle  13684  prdsless  13685  sectfval  13977  sectss  13978  ltbval  16532  opsrle  16536  lmfval  17296  isphtpc  19019  bcthlem1  19277  bcthlem5  19281  lgsquadlem1  21138  lgsquadlem2  21139  lgsquadlem3  21140  inftmrel  24250  isinftm  24251  metidval  24285  metidss  24286  faeval  24597  filnetlem2  26408  pellexlem3  26894  pellexlem4  26895  pellexlem5  26896  pellex  26898  lcvfbr  29818  cmtfvalN  30008  cvrfval  30066  dicssdvh  31984
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-in 3327  df-ss 3334  df-opab 4267  df-xp 4884
  Copyright terms: Public domain W3C validator