Theorem xpss 5640

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	⊢ (𝐴 × 𝐵) ⊆ (V × V)

Proof of Theorem xpss

Step	Hyp	Ref	Expression
1		ssv 3958	. 2 ⊢ 𝐴 ⊆ V
2		ssv 3958	. 2 ⊢ 𝐵 ⊆ V
3		xpss12 5639	. 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 × 𝐵) ⊆ (V × V)

Syntax hints:  Vcvv 3440   ⊆ wss 3901   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-opab 5161  df-xp 5630

This theorem is referenced by:  relxp  5642  copsex2ga  5756  eqbrrdva  5818  relrelss  6231  dff3  7045  eqopi  7969  op1steq  7977  dfoprab4  7999  infxpenlem  9923  nqerf  10841  uzrdgfni  13881  reltrclfv  14940  homarel  17960  relxpchom  18104  frmdplusg  18779  psdmul  22109  upxp  23567  ustrel  24156  utop2nei  24194  utop3cls  24195  fmucndlem  24234  metustrel  24496  xppreima2  32729  df1stres  32783  df2ndres  32784  f1od2  32798  fsuppcurry1  32803  fsuppcurry2  32804  fpwrelmap  32812  metideq  34050  metider  34051  pstmfval  34053  xpinpreima2  34064  tpr2rico  34069  esum2d  34250  dya2iocnrect  34438  mpstssv  35733  txprel  36071  elxp8  37572  mblfinlem1  37854  xrnrel  38563  dihvalrel  41535  rfovcnvf1od  44241  ovolval2lem  46883  sprsymrelfo  47739