Theorem opabssxp 4793

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 4366	. 2 |- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ { <. x , y >. | ( x e. A /\ y e. B ) }
3		df-xp 4725	. 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 4144   X. cxp 4717

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 4146  df-xp 4725

This theorem is referenced by:  brab2ga  4794  dmoprabss  6092  ecopovsym  6786  ecopovtrn  6787  ecopover  6788  ecopovsymg  6789  ecopovtrng  6790  ecopoverg  6791  opabfi  7111  netap  7451  2omotaplemap  7454  2omotaplemst  7455  enqex  7558  ltrelnq  7563  enq0ex  7637  ltrelpr  7703  enrex  7935  ltrelsr  7936  ltrelre  8031  ltrelxr  8218  dvdszrcl  12318  prdsex  13317  prdsval  13321  prdsbaslemss  13322  releqgg  13772  eqgex  13773  aprval  14261  aprap  14265  lmfval  14882  lgsquadlemofi  15770  lgsquadlem1  15771  lgsquadlem2  15772