Theorem xpex 4811

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

Syntax hints:   ∈ wcel 2180  Vcvv 2779   × cxp 4694

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rex 2494  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-opab 4125  df-xp 4702

This theorem is referenced by:  oprabex  6243  oprabex3  6244  mpoexw  6329  fnpm  6773  mapsnf1o2  6813  xpsnen  6948  endisj  6951  xpcomen  6954  xpassen  6957  xpmapenlem  6978  0ct  7242  exmidomni  7277  exmidfodomrlemim  7347  2omotaplemst  7412  enqex  7515  nqex  7518  enq0ex  7594  nq0ex  7595  npex  7628  enrex  7892  addvalex  7999  axcnex  8014  addex  9815  mulex  9816  ixxex  10063  fxnn0nninf  10628  inftonninf  10631  shftfval  11298  nninfct  12528  qnumval  12673  qdenval  12674  qnnen  12968  prdsex  13268  metuex  14484  cnfldstr  14487  cnfldle  14496  znval  14565  znle  14566  znbaslemnn  14568  fnpsr  14596  txuni2  14895  txbas  14897  eltx  14898  txcnp  14910  txcnmpt  14912  txrest  14915  txlm  14918  reldvg  15318