Theorem xpss 5114

Description: A Cartesian product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
xpss

Proof of Theorem xpss

Step	Hyp	Ref	Expression
1		ssv 3523	. 2
2		ssv 3523	. 2
3		xpss12 5113	. 2
4	1, 2, 3	mp2an 672	1

Syntax hints:  cvv 3109  C_wss 3475  X.cxp 5002

This theorem is referenced by:  relxp  5115  copsex2ga  5119  eqbrrdva  5177  relrelss  5536  dff3  6044  eqopi  6834  op1steq  6842  dfoprab4  6857  infxpenlem  8412  nqerf  9329  uzrdgfni  12069  homarel  15363  relxpchom  15450  frmdplusg  16022  upxp  20124  ustrel  20714  utop2nei  20753  utop3cls  20754  fmucndlem  20794  metustrelOLD  21058  metustrel  21059  xppreima2  27488  df1stres  27522  df2ndres  27523  f1od2  27547  fpwrelmap  27556  metideq  27872  metider  27873  pstmfval  27875  xpinpreima2  27889  tpr2rico  27894  dya2iocnrect  28252  mpstssv  28899  txprel  29529  mblfinlem1  30051  bj-elid2  34600  dihvalrel  37006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-opab 4511  df-xp 5010