Theorem opabssxp 4738

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

Syntax hints:   /\ wa 104   e. wcel 2167   C_ wss 3157   {copab 4094   X. cxp 4662

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-in 3163  df-ss 3170  df-opab 4096  df-xp 4670

This theorem is referenced by:  brab2ga  4739  dmoprabss  6008  ecopovsym  6699  ecopovtrn  6700  ecopover  6701  ecopovsymg  6702  ecopovtrng  6703  ecopoverg  6704  opabfi  7008  netap  7337  2omotaplemap  7340  2omotaplemst  7341  enqex  7444  ltrelnq  7449  enq0ex  7523  ltrelpr  7589  enrex  7821  ltrelsr  7822  ltrelre  7917  ltrelxr  8104  dvdszrcl  11974  prdsex  12971  prdsval  12975  prdsbaslemss  12976  releqgg  13426  eqgex  13427  aprval  13914  aprap  13918  lmfval  14512  lgsquadlemofi  15401  lgsquadlem1  15402  lgsquadlem2  15403