Theorem xpex 3266

Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23.

Hypotheses

Ref	Expression
xpex.1	⊢ A ∈ V
xpex.2	⊢ B ∈ V

Assertion

Ref	Expression
xpex	⊢ (A × B) ∈ V

Proof of Theorem xpex

Step	Hyp	Ref	Expression
1		xpex.1	. 2 ⊢ A ∈ V
2		xpex.2	. 2 ⊢ B ∈ V
3		xpexg 3265	. 2 ⊢ ((A ∈ V ⋀ B ∈ V) → (A × B) ∈ V)
4	1, 2, 3	mp2an 699	1 ⊢ (A × B) ∈ V

Syntax hints:   ∈ wcel 960  Vcvv 1814   × cxp 3174

This theorem is referenced by:  oprabex 4025  oprabex3 4028  oprvalex 4047  elpm 4342  map0 4350  map1 4436  xpsnen 4441  endisj 4443  xpcomen 4445  xpassen 4447  xpdom2 4448  xpdom3 4451  xpen 4494  mapxpen 4501  xpmapenlem5 4506  rankxpl 4720  rankxplim 4722  rankxplim2 4723  rankxplim3 4724  rankxpsuc 4725  aceq3 4743  aceq5lem2 4746  aceq5lem3 4747  weth 4797  unxpdomlem 4854  unxpdom2 4856  sucxpdom 4857  uncdadom 4933  cdaassen 4942  xpcdaen 4943  mapcdaen 4944  cdadom1 4945  enqex 5060  nqex 5061  enrex 5190  srex 5191  axcnex 5279  addex 5329  mulex 5330  exp1t 6574  expp1t 6575  serz0 7053  serzcmp0 7055  climconst2 7095  climconst3 7096  climuz0 7108  climaddc1 7118  climmulc2 7129  climsubc2 7131  climcmpc1 7139  iserzcmp0 7143  ser1const 7171  acdc3lem 7487  acdclem 7495  xpnnen 7500  xpomen 7501  qnnen 7504  ruclem9 7519  infxpidmlem1 7553  infxpidmlem9 7561  infxpidmlem10 7562  infxpidmlem12 7564  infmap1 7574  iunctb 7576  infmap2lem2 7582  infmap2 7583  ismeti 7799  metxp 7831  lmclim 7960  metelcls 7962  bcthlem12 8007  bcthlem15 8010  bcthlem30 8025  isgrpi 8039  isgrp2i 8072  vcoprne 8194  sspval 8378  0ofval 8443  ajfval 8465  hvmulex 8876  hlim0 9100  hlimcau 9102  hlimuni 9104

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-opab 2672  df-xp 3190  df-rel 3191

Copyright terms: Public domain