Theorem xpss 5149

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

Syntax hints:  Vcvv 3173   ⊆ wss 3540   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044

This theorem is referenced by:  relxp  5150  copsex2ga  5154  eqbrrdva  5213  relrelss  5576  dff3  6280  eqopi  7093  op1steq  7101  dfoprab4  7116  infxpenlem  8719  nqerf  9631  uzrdgfni  12619  reltrclfv  13606  homarel  16509  relxpchom  16644  frmdplusg  17214  upxp  21236  ustrel  21825  utop2nei  21864  utop3cls  21865  fmucndlem  21905  metustrel  22167  xppreima2  28830  df1stres  28864  df2ndres  28865  f1od2  28887  fpwrelmap  28896  metideq  29264  metider  29265  pstmfval  29267  xpinpreima2  29281  tpr2rico  29286  esum2d  29482  dya2iocnrect  29670  mpstssv  30690  txprel  31156  bj-elid2  32263  elxp8  32395  mblfinlem1  32616  dihvalrel  35586  rfovcnvf1od  37318  ovolval2lem  39533