Theorem xpss 5632

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

Syntax hints:  Vcvv 3436   ⊆ wss 3902   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-opab 5154  df-xp 5622

This theorem is referenced by:  relxp  5634  copsex2ga  5747  eqbrrdva  5809  relrelss  6220  dff3  7033  eqopi  7957  op1steq  7965  dfoprab4  7987  infxpenlem  9901  nqerf  10818  uzrdgfni  13862  reltrclfv  14921  homarel  17940  relxpchom  18084  frmdplusg  18759  psdmul  22079  upxp  23536  ustrel  24125  utop2nei  24163  utop3cls  24164  fmucndlem  24203  metustrel  24465  xppreima2  32628  df1stres  32680  df2ndres  32681  f1od2  32697  fsuppcurry1  32702  fsuppcurry2  32703  fpwrelmap  32711  metideq  33901  metider  33902  pstmfval  33904  xpinpreima2  33915  tpr2rico  33920  esum2d  34101  dya2iocnrect  34289  mpstssv  35571  txprel  35912  elxp8  37404  mblfinlem1  37696  xrnrel  38400  dihvalrel  41317  rfovcnvf1od  44036  ovolval2lem  46680  sprsymrelfo  47527