Theorem xpss 5666

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

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3895   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656

This theorem is used by:  relxp  5668  copsex2ga  5784  eqbrrdva  5846  relrelss  6275  dff3  7100  eqopi  8037  op1steq  8045  dfoprab4  8066  f1od2  8110  infxpenlem  10095  nqerf  11018  uzrdgfni  14104  reltrclfv  15175  homarel  18216  relxpchom  18360  frmdplusg  19055  psdmul  22492  upxp  23947  ustrel  24536  utop2nei  24574  utop3cls  24575  fmucndlem  24614  metustrel  24876  xppreima2  33292  df1stres  33344  df2ndres  33345  fsuppcurry1  33362  fsuppcurry2  33363  fpwrelmap  33371  metideq  34571  metider  34572  pstmfval  34574  xpinpreima2  34585  tpr2rico  34590  esum2d  34771  dya2iocnrect  34959  mpstssv  36390  txprel  36733  elxp8  38387  mblfinlem1  38668  xrnrel  39407  dihvalrel  42429  rfovcnvf1od  45097  ovolval2lem  47746  sprsymrelfo  48672