Theorem xpss 5661

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 5660	. 2 ⊢ ((𝐴 ⊆ V ∧ 𝐵 ⊆ V) → (𝐴 × 𝐵) ⊆ (V × V))
4	1, 2, 3	mp2an 702	1 ⊢ (𝐴 × 𝐵) ⊆ (V × V)

Syntax hints:  Vcvv 3453   ⊆ wss 3904   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-opab 5162  df-xp 5651

This theorem is referenced by:  relxp  5663  copsex2ga  5778  eqbrrdva  5839  relrelss  6256  dff3  7077  eqopi  8002  op1steq  8010  dfoprab4  8032  infxpenlem  9966  nqerf  10885  uzrdgfni  13968  reltrclfv  15027  homarel  18052  relxpchom  18196  frmdplusg  18871  psdmul  22211  upxp  23663  ustrel  24252  utop2nei  24290  utop3cls  24291  fmucndlem  24330  metustrel  24592  xppreima2  32803  df1stres  32856  df2ndres  32857  f1od2  32871  fsuppcurry1  32876  fsuppcurry2  32877  fpwrelmap  32885  metideq  34151  metider  34152  pstmfval  34154  xpinpreima2  34165  tpr2rico  34170  esum2d  34351  dya2iocnrect  34539  mpstssv  35853  txprel  36191  elxp8  37829  mblfinlem1  38120  xrnrel  38845  dihvalrel  41867  rfovcnvf1od  44544  ovolval2lem  47181  sprsymrelfo  48067