Theorem xpss 5639

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

Syntax hints:  Vcvv 3438   ⊆ wss 3905   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-opab 5158  df-xp 5629

This theorem is referenced by:  relxp  5641  copsex2ga  5754  eqbrrdva  5816  relrelss  6225  dff3  7038  eqopi  7967  op1steq  7975  dfoprab4  7997  infxpenlem  9926  nqerf  10843  uzrdgfni  13883  reltrclfv  14942  homarel  17961  relxpchom  18105  frmdplusg  18746  psdmul  22069  upxp  23526  ustrel  24115  utop2nei  24154  utop3cls  24155  fmucndlem  24194  metustrel  24456  xppreima2  32608  df1stres  32660  df2ndres  32661  f1od2  32677  fsuppcurry1  32681  fsuppcurry2  32682  fpwrelmap  32689  metideq  33859  metider  33860  pstmfval  33862  xpinpreima2  33873  tpr2rico  33878  esum2d  34059  dya2iocnrect  34248  mpstssv  35511  txprel  35852  elxp8  37344  mblfinlem1  37636  xrnrel  38340  dihvalrel  41258  rfovcnvf1od  43977  ovolval2lem  46625  sprsymrelfo  47482