Theorem xpex 4834

Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)

Hypotheses

Ref	Expression
xpex.1	⊢ 𝐴 ∈ V
xpex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
xpex	⊢ (𝐴 × 𝐵) ∈ V

Proof of Theorem xpex

Step	Hyp	Ref	Expression
1		xpex.1	. 2 ⊢ 𝐴 ∈ V
2		xpex.2	. 2 ⊢ 𝐵 ∈ V
3		xpexg 4833	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
4	1, 2, 3	mp2an 426	1 ⊢ (𝐴 × 𝐵) ∈ V

Syntax hints:   ∈ wcel 2200  Vcvv 2799   × cxp 4717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-opab 4146  df-xp 4725

This theorem is referenced by:  oprabex  6279  oprabex3  6280  mpoexw  6365  fnpm  6811  mapsnf1o2  6851  xpsnen  6988  endisj  6991  xpcomen  6994  xpassen  6997  xpmapenlem  7018  0ct  7282  exmidomni  7317  exmidfodomrlemim  7387  2omotaplemst  7452  enqex  7555  nqex  7558  enq0ex  7634  nq0ex  7635  npex  7668  enrex  7932  addvalex  8039  axcnex  8054  addex  9855  mulex  9856  ixxex  10103  fxnn0nninf  10669  inftonninf  10672  shftfval  11340  nninfct  12570  qnumval  12715  qdenval  12716  qnnen  13010  prdsex  13310  metuex  14527  cnfldstr  14530  cnfldle  14539  znval  14608  znle  14609  znbaslemnn  14611  fnpsr  14639  txuni2  14938  txbas  14940  eltx  14941  txcnp  14953  txcnmpt  14955  txrest  14958  txlm  14961  reldvg  15361