Theorem xpss 5605

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

Syntax hints:  Vcvv 3432   ⊆ wss 3887   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595

This theorem is referenced by:  relxp  5607  copsex2ga  5717  eqbrrdva  5778  relrelss  6176  dff3  6976  eqopi  7867  op1steq  7875  dfoprab4  7895  infxpenlem  9769  nqerf  10686  uzrdgfni  13678  reltrclfv  14728  homarel  17751  relxpchom  17898  frmdplusg  18493  upxp  22774  ustrel  23363  utop2nei  23402  utop3cls  23403  fmucndlem  23443  metustrel  23708  xppreima2  30988  df1stres  31036  df2ndres  31037  f1od2  31056  fsuppcurry1  31060  fsuppcurry2  31061  fpwrelmap  31068  metideq  31843  metider  31844  pstmfval  31846  xpinpreima2  31857  tpr2rico  31862  esum2d  32061  dya2iocnrect  32248  mpstssv  33501  txprel  34181  elxp8  35542  mblfinlem1  35814  xrnrel  36503  dihvalrel  39293  rfovcnvf1od  41612  ovolval2lem  44181  sprsymrelfo  44949