Theorem opabssxp 5193

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

Step	Hyp	Ref	Expression
1		simpl 473	. . 3 |- ( ( ( x e. A /\ y e. B ) /\ ph ) -> ( x e. A /\ y e. B ) )
2	1	ssopab2i 5003	. 2 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ { <. x , y >. | ( x e. A /\ y e. B ) }
3		df-xp 5120	. 2 |- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
4	2, 3	sseqtr4i 3638	1 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )

Syntax hints:   /\ wa 384   e. wcel 1990   C_ wss 3574   {copab 4712   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120

This theorem is referenced by:  brab2a  5194  dmoprabss  6742  ecopovsym  7849  ecopovtrn  7850  ecopover  7851  ecopoverOLD  7852  enqex  9744  lterpq  9792  ltrelpr  9820  enrex  9888  ltrelsr  9889  ltrelre  9955  ltrelxr  10099  rlimpm  14231  dvdszrcl  14988  prdsle  16122  prdsless  16123  sectfval  16411  sectss  16412  ltbval  19471  opsrle  19475  lmfval  21036  isphtpc  22793  bcthlem1  23121  bcthlem5  23125  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  ishlg  25497  perpln1  25605  perpln2  25606  isperp  25607  iscgra  25701  isinag  25729  isleag  25733  inftmrel  29734  isinftm  29735  metidval  29933  metidss  29934  faeval  30309  filnetlem2  32374  areacirc  33505  lcvfbr  34307  cmtfvalN  34497  cvrfval  34555  dicssdvh  36475  pellexlem3  37395  pellexlem4  37396  pellexlem5  37397  pellex  37399  rfovcnvf1od  38298  fsovrfovd  38303