Theorem xpex 4844

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 4842	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
4	1, 2, 3	mp2an 426	1 ⊢ (𝐴 × 𝐵) ∈ V

Syntax hints:   ∈ wcel 2201  Vcvv 2801   × cxp 4725

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-opab 4152  df-xp 4733

This theorem is referenced by:  oprabex  6295  oprabex3  6296  mpoexw  6383  fnpm  6830  mapsnf1o2  6870  xpsnen  7010  endisj  7013  xpcomen  7016  xpassen  7019  xpmapenlem  7040  0ct  7311  exmidomni  7346  exmidfodomrlemim  7417  2omotaplemst  7482  enqex  7585  nqex  7588  enq0ex  7664  nq0ex  7665  npex  7698  enrex  7962  addvalex  8069  axcnex  8084  addex  9891  mulex  9892  ixxex  10139  fxnn0nninf  10707  inftonninf  10710  shftfval  11404  nninfct  12635  qnumval  12780  qdenval  12781  qnnen  13075  prdsex  13375  metuex  14593  cnfldstr  14596  cnfldle  14605  znval  14674  znle  14675  znbaslemnn  14677  fnpsr  14705  txuni2  15009  txbas  15011  eltx  15012  txcnp  15024  txcnmpt  15026  txrest  15029  txlm  15032  reldvg  15432