Theorem xpss 5654

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

Syntax hints:  Vcvv 3447   ⊆ wss 3914   × cxp 5636

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 3449  df-ss 3931  df-opab 5170  df-xp 5644

This theorem is referenced by:  relxp  5656  copsex2ga  5770  eqbrrdva  5833  relrelss  6246  dff3  7072  eqopi  8004  op1steq  8012  dfoprab4  8034  infxpenlem  9966  nqerf  10883  uzrdgfni  13923  reltrclfv  14983  homarel  17998  relxpchom  18142  frmdplusg  18781  psdmul  22053  upxp  23510  ustrel  24099  utop2nei  24138  utop3cls  24139  fmucndlem  24178  metustrel  24440  xppreima2  32575  df1stres  32627  df2ndres  32628  f1od2  32644  fsuppcurry1  32648  fsuppcurry2  32649  fpwrelmap  32656  metideq  33883  metider  33884  pstmfval  33886  xpinpreima2  33897  tpr2rico  33902  esum2d  34083  dya2iocnrect  34272  mpstssv  35526  txprel  35867  elxp8  37359  mblfinlem1  37651  xrnrel  38355  dihvalrel  41273  rfovcnvf1od  43993  ovolval2lem  46641  sprsymrelfo  47498