Theorem xpss 5635

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

Syntax hints:  Vcvv 3437   ⊆ wss 3898   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-opab 5156  df-xp 5625

This theorem is referenced by:  relxp  5637  copsex2ga  5751  eqbrrdva  5813  relrelss  6225  dff3  7039  eqopi  7963  op1steq  7971  dfoprab4  7993  infxpenlem  9911  nqerf  10828  uzrdgfni  13867  reltrclfv  14926  homarel  17945  relxpchom  18089  frmdplusg  18764  psdmul  22082  upxp  23539  ustrel  24128  utop2nei  24166  utop3cls  24167  fmucndlem  24206  metustrel  24468  xppreima2  32635  df1stres  32689  df2ndres  32690  f1od2  32706  fsuppcurry1  32711  fsuppcurry2  32712  fpwrelmap  32720  metideq  33927  metider  33928  pstmfval  33930  xpinpreima2  33941  tpr2rico  33946  esum2d  34127  dya2iocnrect  34315  mpstssv  35604  txprel  35942  elxp8  37436  mblfinlem1  37717  xrnrel  38426  dihvalrel  41398  rfovcnvf1od  44121  ovolval2lem  46765  sprsymrelfo  47621