Theorem xpex 3260

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

Hypotheses

Ref	Expression
xpex.1	|- A e. V
xpex.2	|- B e. V

Assertion

Ref	Expression
xpex	|- (A X. B) e. V

Proof of Theorem xpex

Step	Hyp	Ref	Expression
1		xpex.1	. 2 |- A e. V
2		xpex.2	. 2 |- B e. V
3		xpexg 3259	. 2 |- ((A e. V /\ B e. V) -> (A X. B) e. V)
4	1, 2, 3	mp2an 697	1 |- (A X. B) e. V

Syntax hints:   e. wcel 958  Vcvv 1811   X. cxp 3168

This theorem is referenced by:  oprabex 4019  oprabex3 4022  oprvalex 4041  elpm 4336  map0 4344  map1 4430  xpsnen 4435  endisj 4437  xpcomen 4439  xpassen 4441  xpdom2 4442  xpdom3 4445  xpen 4488  mapxpen 4495  xpmapenlem5 4500  rankxpl 4710  rankxplim 4712  rankxplim2 4713  rankxplim3 4714  rankxpsuc 4715  aceq3 4733  aceq5lem2 4736  aceq5lem3 4737  weth 4787  unxpdomlem 4843  unxpdom2 4845  sucxpdom 4846  uncdadom 4921  cdaassen 4930  xpcdaen 4931  mapcdaen 4932  cdadom1 4933  enqex 5048  nqex 5049  enrex 5178  srex 5179  axcnex 5267  addex 5317  mulex 5318  exp1t 6573  expp1t 6574  serz0 7053  serzcmp0 7055  climconst2 7095  climconst3 7096  climuz0 7108  climaddc1 7118  climmulc2 7129  climsubc2 7131  climcmpc1 7139  iserzcmp0 7143  ser1const 7171  acdc3lem 7486  acdclem 7494  xpnnen 7499  xpomen 7500  qnnen 7503  ruclem9 7518  infxpidmlem1 7552  infxpidmlem9 7560  infxpidmlem10 7561  infxpidmlem12 7563  infmap1 7573  iunctb 7575  infmap2lem2 7580  infmap2 7581  ismeti 7802  metxp 7834  lmclim 7963  metelcls 7965  bcthlem12 8010  bcthlem15 8013  bcthlem30 8028  isgrpi 8042  isgrp2i 8076  vcoprne 8198  sspval 8382  0ofval 8447  ajfval 8469  hvmulex 8881  hlim0 9105  hlimcau 9107  hlimuni 9109

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-opab 2667  df-xp 3184  df-rel 3185

Copyright terms: Public domain