Theorem xpss 5670

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

Syntax hints:  Vcvv 3459   ⊆ wss 3926   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660

This theorem is referenced by:  relxp  5672  copsex2ga  5786  eqbrrdva  5849  relrelss  6262  dff3  7089  eqopi  8022  op1steq  8030  dfoprab4  8052  infxpenlem  10025  nqerf  10942  uzrdgfni  13974  reltrclfv  15034  homarel  18047  relxpchom  18191  frmdplusg  18830  psdmul  22102  upxp  23559  ustrel  24148  utop2nei  24187  utop3cls  24188  fmucndlem  24227  metustrel  24489  xppreima2  32575  df1stres  32627  df2ndres  32628  f1od2  32644  fsuppcurry1  32648  fsuppcurry2  32649  fpwrelmap  32656  metideq  33870  metider  33871  pstmfval  33873  xpinpreima2  33884  tpr2rico  33889  esum2d  34070  dya2iocnrect  34259  mpstssv  35507  txprel  35843  elxp8  37335  mblfinlem1  37627  xrnrel  38337  dihvalrel  41244  rfovcnvf1od  43975  ovolval2lem  46620  sprsymrelfo  47459