Theorem xpss 5596

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

Syntax hints:  Vcvv 3422   ⊆ wss 3883   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586

This theorem is referenced by:  relxp  5598  copsex2ga  5706  eqbrrdva  5767  relrelss  6165  dff3  6958  eqopi  7840  op1steq  7848  dfoprab4  7868  infxpenlem  9700  nqerf  10617  uzrdgfni  13606  reltrclfv  14656  homarel  17667  relxpchom  17814  frmdplusg  18408  upxp  22682  ustrel  23271  utop2nei  23310  utop3cls  23311  fmucndlem  23351  metustrel  23614  xppreima2  30889  df1stres  30938  df2ndres  30939  f1od2  30958  fsuppcurry1  30962  fsuppcurry2  30963  fpwrelmap  30970  metideq  31745  metider  31746  pstmfval  31748  xpinpreima2  31759  tpr2rico  31764  esum2d  31961  dya2iocnrect  32148  mpstssv  33401  txprel  34108  elxp8  35469  mblfinlem1  35741  xrnrel  36430  dihvalrel  39220  rfovcnvf1od  41501  ovolval2lem  44071  sprsymrelfo  44837