Theorem opabssxp 4748

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

Step	Hyp	Ref	Expression
1		simpl 109	. . 3 |- ( ( ( x e. A /\ y e. B ) /\ ph ) -> ( x e. A /\ y e. B ) )
2	1	ssopab2i 4323	. 2 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ { <. x , y >. | ( x e. A /\ y e. B ) }
3		df-xp 4680	. 2 |- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
4	2, 3	sseqtrri 3227	1 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )

Syntax hints:   /\ wa 104   e. wcel 2175   C_ wss 3165   {copab 4103   X. cxp 4672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-in 3171  df-ss 3178  df-opab 4105  df-xp 4680

This theorem is referenced by:  brab2ga  4749  dmoprabss  6026  ecopovsym  6717  ecopovtrn  6718  ecopover  6719  ecopovsymg  6720  ecopovtrng  6721  ecopoverg  6722  opabfi  7034  netap  7365  2omotaplemap  7368  2omotaplemst  7369  enqex  7472  ltrelnq  7477  enq0ex  7551  ltrelpr  7617  enrex  7849  ltrelsr  7850  ltrelre  7945  ltrelxr  8132  dvdszrcl  12045  prdsex  13043  prdsval  13047  prdsbaslemss  13048  releqgg  13498  eqgex  13499  aprval  13986  aprap  13990  lmfval  14606  lgsquadlemofi  15495  lgsquadlem1  15496  lgsquadlem2  15497