Theorem xpss 5716

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

Syntax hints:  Vcvv 3488   ⊆ wss 3976   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706

This theorem is referenced by:  relxp  5718  copsex2ga  5831  eqbrrdva  5894  relrelss  6304  dff3  7134  eqopi  8066  op1steq  8074  dfoprab4  8096  infxpenlem  10082  nqerf  10999  uzrdgfni  14009  reltrclfv  15066  homarel  18103  relxpchom  18250  frmdplusg  18889  psdmul  22193  upxp  23652  ustrel  24241  utop2nei  24280  utop3cls  24281  fmucndlem  24321  metustrel  24586  xppreima2  32669  df1stres  32715  df2ndres  32716  f1od2  32735  fsuppcurry1  32739  fsuppcurry2  32740  fpwrelmap  32747  metideq  33839  metider  33840  pstmfval  33842  xpinpreima2  33853  tpr2rico  33858  esum2d  34057  dya2iocnrect  34246  mpstssv  35507  txprel  35843  elxp8  37337  mblfinlem1  37617  xrnrel  38329  dihvalrel  41236  rfovcnvf1od  43966  ovolval2lem  46564  sprsymrelfo  47371