Theorem xpss 5641

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

Syntax hints:  Vcvv 3432   ⊆ wss 3890   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-opab 5142  df-xp 5631

This theorem is referenced by:  relxp  5643  copsex2ga  5757  eqbrrdva  5818  relrelss  6231  dff3  7048  eqopi  7974  op1steq  7982  dfoprab4  8004  infxpenlem  9933  nqerf  10851  uzrdgfni  13918  reltrclfv  14977  homarel  18001  relxpchom  18145  frmdplusg  18820  psdmul  22161  upxp  23613  ustrel  24202  utop2nei  24240  utop3cls  24241  fmucndlem  24280  metustrel  24542  xppreima2  32750  df1stres  32803  df2ndres  32804  f1od2  32818  fsuppcurry1  32823  fsuppcurry2  32824  fpwrelmap  32832  metideq  34084  metider  34085  pstmfval  34087  xpinpreima2  34098  tpr2rico  34103  esum2d  34284  dya2iocnrect  34472  mpstssv  35774  txprel  36112  elxp8  37740  mblfinlem1  38031  xrnrel  38756  dihvalrel  41778  rfovcnvf1od  44455  ovolval2lem  47093  sprsymrelfo  47979