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

Theorem opabssxp 5064
Description: An abstraction relation is a subset of a related Cartesian 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 457 . . 3  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( x  e.  A  /\  y  e.  B
) )
21ssopab2i 4765 . 2  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
3 df-xp 4995 . 2  |-  ( A  X.  B )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  B ) }
42, 3sseqtr4i 3522 1  |-  { <. x ,  y >.  |  ( ( x  e.  A  /\  y  e.  B
)  /\  ph ) } 
C_  ( A  X.  B )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1804    C_ wss 3461   {copab 4494    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-opab 4496  df-xp 4995
This theorem is referenced by:  brab2ga  5065  dmoprabss  6369  ecopovsym  7415  ecopovtrn  7416  ecopover  7417  enqex  9303  lterpq  9351  ltrelpr  9379  enrex  9447  ltrelsr  9448  ltrelre  9514  ltrelxr  9651  rlimpm  13304  dvdszrcl  13972  prdsle  14840  prdsless  14841  sectfval  15127  sectss  15128  ltbval  18114  opsrle  18118  lmfval  19710  isphtpc  21471  bcthlem1  21740  bcthlem5  21744  lgsquadlem1  23605  lgsquadlem2  23606  lgsquadlem3  23607  ishlg  23962  perpln1  24063  perpln2  24064  isperp  24065  iscgra  24145  inftmrel  27701  isinftm  27702  metidval  27846  metidss  27847  faeval  28195  filnetlem2  30172  pellexlem3  30742  pellexlem4  30743  pellexlem5  30744  pellex  30746  lcvfbr  34485  cmtfvalN  34675  cvrfval  34733  dicssdvh  36653
  Copyright terms: Public domain W3C validator