Theorem xpss 5682

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

This proof depends on syntax axioms:  Vcvv 3458   ⊆ wss 3908   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-opab 5179  df-xp 5672

This theorem is used by:  relxp  5684  copsex2ga  5799  eqbrrdva  5860  relrelss  6280  dff3  7102  eqopi  8031  op1steq  8039  dfoprab4  8061  infxpenlem  10016  nqerf  10933  uzrdgfni  14014  reltrclfv  15080  homarel  18118  relxpchom  18262  frmdplusg  18944  psdmul  22366  upxp  23817  ustrel  24406  utop2nei  24444  utop3cls  24445  fmucndlem  24484  metustrel  24746  xppreima2  33033  df1stres  33086  df2ndres  33087  f1od2  33101  fsuppcurry1  33106  fsuppcurry2  33107  fpwrelmap  33115  metideq  34314  metider  34315  pstmfval  34317  xpinpreima2  34328  tpr2rico  34333  esum2d  34514  dya2iocnrect  34703  mpstssv  36052  txprel  36390  elxp8  38058  mblfinlem1  38349  xrnrel  39072  dihvalrel  42094  rfovcnvf1od  44771  ovolval2lem  47398  sprsymrelfo  48287