Theorem xpss 5671

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

This proof depends on syntax axioms:  Vcvv 3454   ⊆ wss 3900   × cxp 5653

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-opab 5171  df-xp 5661

This theorem is used by:  relxp  5673  copsex2ga  5790  eqbrrdva  5854  relrelss  6293  dff3  7124  eqopi  8061  op1steq  8069  dfoprab4  8091  f1od2  8135  infxpenlem  10119  nqerf  11042  uzrdgfni  14128  reltrclfv  15199  homarel  18240  relxpchom  18384  frmdplusg  19079  psdmul  22517  upxp  23972  ustrel  24561  utop2nei  24599  utop3cls  24600  fmucndlem  24639  metustrel  24901  xppreima2  33317  df1stres  33368  df2ndres  33369  fsuppcurry1  33386  fsuppcurry2  33387  fpwrelmap  33395  metideq  34595  metider  34596  pstmfval  34598  xpinpreima2  34609  tpr2rico  34614  esum2d  34795  dya2iocnrect  34983  mpstssv  36471  txprel  36819  elxp8  38486  mblfinlem1  38767  xrnrel  39506  dihvalrel  42528  rfovcnvf1od  45196  ovolval2lem  47858  sprsymrelfo  48784