Theorem xpss 5552

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

Syntax hints:  Vcvv 3398   ⊆ wss 3853   × cxp 5534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-opab 5102  df-xp 5542

This theorem is referenced by:  relxp  5554  copsex2ga  5662  eqbrrdva  5723  relrelss  6116  dff3  6897  eqopi  7775  op1steq  7783  dfoprab4  7803  infxpenlem  9592  nqerf  10509  uzrdgfni  13496  reltrclfv  14545  homarel  17496  relxpchom  17642  frmdplusg  18235  upxp  22474  ustrel  23063  utop2nei  23102  utop3cls  23103  fmucndlem  23142  metustrel  23404  xppreima2  30661  df1stres  30710  df2ndres  30711  f1od2  30730  fsuppcurry1  30734  fsuppcurry2  30735  fpwrelmap  30742  metideq  31511  metider  31512  pstmfval  31514  xpinpreima2  31525  tpr2rico  31530  esum2d  31727  dya2iocnrect  31914  mpstssv  33168  txprel  33867  elxp8  35228  mblfinlem1  35500  xrnrel  36189  dihvalrel  38979  rfovcnvf1od  41230  ovolval2lem  43799  sprsymrelfo  44565