Theorem xpss 5282

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

Syntax hints:  Vcvv 3340   ⊆ wss 3715   × cxp 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729  df-opab 4865  df-xp 5272

This theorem is referenced by:  relxp  5283  copsex2ga  5387  eqbrrdva  5447  relrelss  5820  dff3  6535  eqopi  7369  op1steq  7377  dfoprab4  7392  infxpenlem  9026  nqerf  9944  uzrdgfni  12951  reltrclfv  13957  homarel  16887  relxpchom  17022  frmdplusg  17592  upxp  21628  ustrel  22216  utop2nei  22255  utop3cls  22256  fmucndlem  22296  metustrel  22558  xppreima2  29759  df1stres  29790  df2ndres  29791  f1od2  29808  fpwrelmap  29817  metideq  30245  metider  30246  pstmfval  30248  xpinpreima2  30262  tpr2rico  30267  esum2d  30464  dya2iocnrect  30652  mpstssv  31743  txprel  32292  bj-elid2  33397  elxp8  33530  mblfinlem1  33759  xrnrel  34458  dihvalrel  37070  rfovcnvf1od  38800  ovolval2lem  41363  sprsymrelfo  42257