Theorem opabssxp 4193

Description: An abstraction relation is a subset of a related cross product.

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

Proof of Theorem opabssxp

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

Syntax hints:   /\ wa 337   e. wcel 1588   C_ wss 2827  {copab 3565   X. cxp 4117

This theorem is referenced by:  dmoprabss 5025  ecopoprdm 5529  ecopoprsym 5530  ecopoprtrn 5531  enqex 6566  ltrelpq 6569  ltrelpr 6619  enrex 6696  ltrelsr 6698  ltrelre 6770  lmfval 10069  bcthlem12 10154  bcthlem15 10157  dmhmph 15643  rnhmph 15644  tlmval 16727  phtpcval 16882  cmtfval 17604  cvrfval 17660

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-opab 3566  df-xp 4133

Copyright terms: Public domain