Theorem xpss 5675

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

This proof depends on syntax axioms:  Vcvv 3453   ⊆ wss 3902   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665

This theorem is used by:  relxp  5677  copsex2ga  5792  eqbrrdva  5853  relrelss  6274  dff3  7097  eqopi  8026  op1steq  8034  dfoprab4  8056  infxpenlem  10020  nqerf  10943  uzrdgfni  14026  reltrclfv  15094  homarel  18131  relxpchom  18275  frmdplusg  18969  psdmul  22400  upxp  23855  ustrel  24444  utop2nei  24482  utop3cls  24483  fmucndlem  24522  metustrel  24784  xppreima2  33132  df1stres  33184  df2ndres  33185  f1od2  33198  fsuppcurry1  33203  fsuppcurry2  33204  fpwrelmap  33212  metideq  34411  metider  34412  pstmfval  34414  xpinpreima2  34425  tpr2rico  34430  esum2d  34611  dya2iocnrect  34800  mpstssv  36126  txprel  36464  elxp8  38133  mblfinlem1  38414  xrnrel  39138  dihvalrel  42160  rfovcnvf1od  44852  ovolval2lem  47479  sprsymrelfo  48405