Theorem xpss 5636

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

Syntax hints:  Vcvv 3441   ⊆ wss 3898   × cxp 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-opab 5155  df-xp 5626

This theorem is referenced by:  relxp  5638  copsex2ga  5749  eqbrrdva  5811  relrelss  6211  dff3  7032  eqopi  7935  op1steq  7943  dfoprab4  7963  infxpenlem  9870  nqerf  10787  uzrdgfni  13779  reltrclfv  14827  homarel  17848  relxpchom  17995  frmdplusg  18589  upxp  22880  ustrel  23469  utop2nei  23508  utop3cls  23509  fmucndlem  23549  metustrel  23814  xppreima2  31275  df1stres  31323  df2ndres  31324  f1od2  31343  fsuppcurry1  31347  fsuppcurry2  31348  fpwrelmap  31355  metideq  32141  metider  32142  pstmfval  32144  xpinpreima2  32155  tpr2rico  32160  esum2d  32359  dya2iocnrect  32548  mpstssv  33800  txprel  34277  elxp8  35655  mblfinlem1  35927  xrnrel  36648  dihvalrel  39555  rfovcnvf1od  41942  ovolval2lem  44527  sprsymrelfo  45309