Theorem xpss 5657

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

Syntax hints:  Vcvv 3450   ⊆ wss 3917   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647

This theorem is referenced by:  relxp  5659  copsex2ga  5773  eqbrrdva  5836  relrelss  6249  dff3  7075  eqopi  8007  op1steq  8015  dfoprab4  8037  infxpenlem  9973  nqerf  10890  uzrdgfni  13930  reltrclfv  14990  homarel  18005  relxpchom  18149  frmdplusg  18788  psdmul  22060  upxp  23517  ustrel  24106  utop2nei  24145  utop3cls  24146  fmucndlem  24185  metustrel  24447  xppreima2  32582  df1stres  32634  df2ndres  32635  f1od2  32651  fsuppcurry1  32655  fsuppcurry2  32656  fpwrelmap  32663  metideq  33890  metider  33891  pstmfval  33893  xpinpreima2  33904  tpr2rico  33909  esum2d  34090  dya2iocnrect  34279  mpstssv  35533  txprel  35874  elxp8  37366  mblfinlem1  37658  xrnrel  38362  dihvalrel  41280  rfovcnvf1od  44000  ovolval2lem  46648  sprsymrelfo  47502