Theorem xpss 5701

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

Syntax hints:  Vcvv 3480   ⊆ wss 3951   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691

This theorem is referenced by:  relxp  5703  copsex2ga  5817  eqbrrdva  5880  relrelss  6293  dff3  7120  eqopi  8050  op1steq  8058  dfoprab4  8080  infxpenlem  10053  nqerf  10970  uzrdgfni  13999  reltrclfv  15056  homarel  18081  relxpchom  18226  frmdplusg  18867  psdmul  22170  upxp  23631  ustrel  24220  utop2nei  24259  utop3cls  24260  fmucndlem  24300  metustrel  24565  xppreima2  32661  df1stres  32713  df2ndres  32714  f1od2  32732  fsuppcurry1  32736  fsuppcurry2  32737  fpwrelmap  32744  metideq  33892  metider  33893  pstmfval  33895  xpinpreima2  33906  tpr2rico  33911  esum2d  34094  dya2iocnrect  34283  mpstssv  35544  txprel  35880  elxp8  37372  mblfinlem1  37664  xrnrel  38374  dihvalrel  41281  rfovcnvf1od  44017  ovolval2lem  46658  sprsymrelfo  47484