Theorem xpss 5704

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

Syntax hints:  Vcvv 3477   ⊆ wss 3962   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694

This theorem is referenced by:  relxp  5706  copsex2ga  5819  eqbrrdva  5882  relrelss  6294  dff3  7119  eqopi  8048  op1steq  8056  dfoprab4  8078  infxpenlem  10050  nqerf  10967  uzrdgfni  13995  reltrclfv  15052  homarel  18089  relxpchom  18236  frmdplusg  18879  psdmul  22187  upxp  23646  ustrel  24235  utop2nei  24274  utop3cls  24275  fmucndlem  24315  metustrel  24580  xppreima2  32667  df1stres  32718  df2ndres  32719  f1od2  32738  fsuppcurry1  32742  fsuppcurry2  32743  fpwrelmap  32750  metideq  33853  metider  33854  pstmfval  33856  xpinpreima2  33867  tpr2rico  33872  esum2d  34073  dya2iocnrect  34262  mpstssv  35523  txprel  35860  elxp8  37353  mblfinlem1  37643  xrnrel  38354  dihvalrel  41261  rfovcnvf1od  43993  ovolval2lem  46598  sprsymrelfo  47421