Theorem opabssxp 4792

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 4365	. 2 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ { <. x , y >. | ( x e. A /\ y e. B ) }
3		df-xp 4724	. 2 |- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
4	2, 3	sseqtrri 3259	1 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )

Syntax hints:   /\ wa 104   e. wcel 2200   C_ wss 3197   {copab 4143   X. cxp 4716

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3203  df-ss 3210  df-opab 4145  df-xp 4724

This theorem is referenced by:  brab2ga  4793  dmoprabss  6085  ecopovsym  6776  ecopovtrn  6777  ecopover  6778  ecopovsymg  6779  ecopovtrng  6780  ecopoverg  6781  opabfi  7096  netap  7436  2omotaplemap  7439  2omotaplemst  7440  enqex  7543  ltrelnq  7548  enq0ex  7622  ltrelpr  7688  enrex  7920  ltrelsr  7921  ltrelre  8016  ltrelxr  8203  dvdszrcl  12298  prdsex  13297  prdsval  13301  prdsbaslemss  13302  releqgg  13752  eqgex  13753  aprval  14240  aprap  14244  lmfval  14860  lgsquadlemofi  15749  lgsquadlem1  15750  lgsquadlem2  15751