Theorem xpss 5648

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 3960	. 2 ⊢ 𝐴 ⊆ V
2		ssv 3960	. 2 ⊢ 𝐵 ⊆ V
3		xpss12 5647	. 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴 × 𝐵) ⊆ (V × V)

Syntax hints:  Vcvv 3442   ⊆ wss 3903   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-opab 5163  df-xp 5638

This theorem is referenced by:  relxp  5650  copsex2ga  5764  eqbrrdva  5826  relrelss  6239  dff3  7054  eqopi  7979  op1steq  7987  dfoprab4  8009  infxpenlem  9935  nqerf  10853  uzrdgfni  13893  reltrclfv  14952  homarel  17972  relxpchom  18116  frmdplusg  18791  psdmul  22121  upxp  23579  ustrel  24168  utop2nei  24206  utop3cls  24207  fmucndlem  24246  metustrel  24508  xppreima2  32740  df1stres  32793  df2ndres  32794  f1od2  32808  fsuppcurry1  32813  fsuppcurry2  32814  fpwrelmap  32822  metideq  34070  metider  34071  pstmfval  34073  xpinpreima2  34084  tpr2rico  34089  esum2d  34270  dya2iocnrect  34458  mpstssv  35752  txprel  36090  elxp8  37620  mblfinlem1  37902  xrnrel  38627  dihvalrel  41649  rfovcnvf1od  44354  ovolval2lem  46995  sprsymrelfo  47851