Theorem xpss 5693

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

Syntax hints:  Vcvv 3475   ⊆ wss 3949   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683

This theorem is referenced by:  relxp  5695  copsex2ga  5808  eqbrrdva  5870  relrelss  6273  dff3  7102  eqopi  8011  op1steq  8019  dfoprab4  8041  infxpenlem  10008  nqerf  10925  uzrdgfni  13923  reltrclfv  14964  homarel  17986  relxpchom  18133  frmdplusg  18735  upxp  23127  ustrel  23716  utop2nei  23755  utop3cls  23756  fmucndlem  23796  metustrel  24061  xppreima2  31876  df1stres  31925  df2ndres  31926  f1od2  31946  fsuppcurry1  31950  fsuppcurry2  31951  fpwrelmap  31958  metideq  32873  metider  32874  pstmfval  32876  xpinpreima2  32887  tpr2rico  32892  esum2d  33091  dya2iocnrect  33280  mpstssv  34530  txprel  34851  elxp8  36252  mblfinlem1  36525  xrnrel  37243  dihvalrel  40150  rfovcnvf1od  42755  ovolval2lem  45359  sprsymrelfo  46165