Theorem xpex 4838

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

Syntax hints:   ∈ wcel 2200  Vcvv 2800   × cxp 4719

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 4203  ax-pow 4260  ax-pr 4295  ax-un 4526

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-opab 4147  df-xp 4727

This theorem is referenced by:  oprabex  6283  oprabex3  6284  mpoexw  6371  fnpm  6818  mapsnf1o2  6858  xpsnen  6998  endisj  7001  xpcomen  7004  xpassen  7007  xpmapenlem  7028  0ct  7295  exmidomni  7330  exmidfodomrlemim  7400  2omotaplemst  7465  enqex  7568  nqex  7571  enq0ex  7647  nq0ex  7648  npex  7681  enrex  7945  addvalex  8052  axcnex  8067  addex  9874  mulex  9875  ixxex  10122  fxnn0nninf  10689  inftonninf  10692  shftfval  11369  nninfct  12599  qnumval  12744  qdenval  12745  qnnen  13039  prdsex  13339  metuex  14556  cnfldstr  14559  cnfldle  14568  znval  14637  znle  14638  znbaslemnn  14640  fnpsr  14668  txuni2  14967  txbas  14969  eltx  14970  txcnp  14982  txcnmpt  14984  txrest  14987  txlm  14990  reldvg  15390