Theorem xpss 5647

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

Syntax hints:  Vcvv 3429   ⊆ wss 3889   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637

This theorem is referenced by:  relxp  5649  copsex2ga  5763  eqbrrdva  5824  relrelss  6237  dff3  7052  eqopi  7978  op1steq  7986  dfoprab4  8008  infxpenlem  9935  nqerf  10853  uzrdgfni  13920  reltrclfv  14979  homarel  18003  relxpchom  18147  frmdplusg  18822  psdmul  22132  upxp  23588  ustrel  24177  utop2nei  24215  utop3cls  24216  fmucndlem  24255  metustrel  24517  xppreima2  32724  df1stres  32777  df2ndres  32778  f1od2  32792  fsuppcurry1  32797  fsuppcurry2  32798  fpwrelmap  32806  metideq  34037  metider  34038  pstmfval  34040  xpinpreima2  34051  tpr2rico  34056  esum2d  34237  dya2iocnrect  34425  mpstssv  35721  txprel  36059  elxp8  37687  mblfinlem1  37978  xrnrel  38703  dihvalrel  41725  rfovcnvf1od  44431  ovolval2lem  47071  sprsymrelfo  47957