Theorem xpss 5679

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

Syntax hints:  Vcvv 3455   ⊆ wss 3906   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-opab 5175  df-xp 5669

This theorem is referenced by:  relxp  5681  copsex2ga  5796  eqbrrdva  5857  relrelss  6276  dff3  7097  eqopi  8023  op1steq  8031  dfoprab4  8053  infxpenlem  9998  nqerf  10916  uzrdgfni  13996  reltrclfv  15056  homarel  18094  relxpchom  18238  frmdplusg  18914  psdmul  22310  upxp  23761  ustrel  24350  utop2nei  24388  utop3cls  24389  fmucndlem  24428  metustrel  24690  xppreima2  32974  df1stres  33027  df2ndres  33028  f1od2  33042  fsuppcurry1  33047  fsuppcurry2  33048  fpwrelmap  33056  metideq  34261  metider  34262  pstmfval  34264  xpinpreima2  34275  tpr2rico  34280  esum2d  34461  dya2iocnrect  34649  mpstssv  36009  txprel  36347  elxp8  37995  mblfinlem1  38286  xrnrel  39009  dihvalrel  42031  rfovcnvf1od  44710  ovolval2lem  47337  sprsymrelfo  48223