Theorem xpss 5667

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

This proof depends on syntax axioms:  Vcvv 3451   ⊆ wss 3899   × cxp 5649

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-opab 5168  df-xp 5657

This theorem is used by:  relxp  5669  copsex2ga  5785  eqbrrdva  5847  relrelss  6268  dff3  7092  eqopi  8026  op1steq  8034  dfoprab4  8055  infxpenlem  10073  nqerf  10996  uzrdgfni  14081  reltrclfv  15150  homarel  18191  relxpchom  18335  frmdplusg  19030  psdmul  22467  upxp  23922  ustrel  24511  utop2nei  24549  utop3cls  24550  fmucndlem  24589  metustrel  24851  xppreima2  33227  df1stres  33279  df2ndres  33280  f1od2  33293  fsuppcurry1  33298  fsuppcurry2  33299  fpwrelmap  33307  metideq  34507  metider  34508  pstmfval  34510  xpinpreima2  34521  tpr2rico  34526  esum2d  34707  dya2iocnrect  34896  mpstssv  36273  txprel  36611  elxp8  38262  mblfinlem1  38543  xrnrel  39282  dihvalrel  42304  rfovcnvf1od  44963  ovolval2lem  47597  sprsymrelfo  48523