Theorem xpss 5654

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

Syntax hints:  Vcvv 3446   ⊆ wss 3913   × cxp 5636

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-opab 5173  df-xp 5644

This theorem is referenced by:  relxp  5656  copsex2ga  5768  eqbrrdva  5830  relrelss  6230  dff3  7055  eqopi  7962  op1steq  7970  dfoprab4  7992  infxpenlem  9958  nqerf  10875  uzrdgfni  13873  reltrclfv  14914  homarel  17936  relxpchom  18083  frmdplusg  18678  upxp  23011  ustrel  23600  utop2nei  23639  utop3cls  23640  fmucndlem  23680  metustrel  23945  xppreima2  31634  df1stres  31685  df2ndres  31686  f1od2  31706  fsuppcurry1  31710  fsuppcurry2  31711  fpwrelmap  31718  metideq  32563  metider  32564  pstmfval  32566  xpinpreima2  32577  tpr2rico  32582  esum2d  32781  dya2iocnrect  32970  mpstssv  34220  txprel  34540  elxp8  35915  mblfinlem1  36188  xrnrel  36908  dihvalrel  39815  rfovcnvf1od  42398  ovolval2lem  45004  sprsymrelfo  45809