Theorem xpss 5682

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

This proof depends on syntax axioms:  Vcvv 3458   ⊆ wss 3908   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-opab 5179  df-xp 5672

This theorem is used by:  relxp  5684  copsex2ga  5799  eqbrrdva  5860  relrelss  6280  dff3  7102  eqopi  8031  op1steq  8039  dfoprab4  8061  infxpenlem  10016  nqerf  10933  uzrdgfni  14014  reltrclfv  15080  homarel  18118  relxpchom  18262  frmdplusg  18938  psdmul  22359  upxp  23810  ustrel  24399  utop2nei  24437  utop3cls  24438  fmucndlem  24477  metustrel  24739  xppreima2  33026  df1stres  33079  df2ndres  33080  f1od2  33094  fsuppcurry1  33099  fsuppcurry2  33100  fpwrelmap  33108  metideq  34307  metider  34308  pstmfval  34310  xpinpreima2  34321  tpr2rico  34326  esum2d  34507  dya2iocnrect  34695  mpstssv  36044  txprel  36382  elxp8  38050  mblfinlem1  38341  xrnrel  39064  dihvalrel  42086  rfovcnvf1od  44763  ovolval2lem  47390  sprsymrelfo  48279