Theorem xpss 5459

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

Syntax hints:  Vcvv 3437   ⊆ wss 3859   × cxp 5441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3866  df-ss 3874  df-opab 5025  df-xp 5449

This theorem is referenced by:  relxp  5461  copsex2ga  5566  eqbrrdva  5626  relrelss  5999  dff3  6729  eqopi  7581  op1steq  7589  dfoprab4  7609  infxpenlem  9285  nqerf  10198  uzrdgfni  13176  reltrclfv  14211  homarel  17125  relxpchom  17260  frmdplusg  17830  upxp  21915  ustrel  22503  utop2nei  22542  utop3cls  22543  fmucndlem  22583  metustrel  22845  xppreima2  30085  df1stres  30127  df2ndres  30128  f1od2  30145  fsuppcurry1  30149  fsuppcurry2  30150  fpwrelmap  30157  metideq  30750  metider  30751  pstmfval  30753  xpinpreima2  30767  tpr2rico  30772  esum2d  30969  dya2iocnrect  31156  mpstssv  32394  txprel  32949  bj-elid2  34028  elxp8  34183  mblfinlem1  34460  xrnrel  35156  dihvalrel  37946  rfovcnvf1od  39835  ovolval2lem  42467  sprsymrelfo  43141