Theorem ifex 4010

Description: Conditional operator existence. (Contributed by NM, 2-Sep-2004.)

Hypotheses

Ref	Expression
dedex.1
dedex.2

Assertion

Ref	Expression
ifex

Proof of Theorem ifex

Step	Hyp	Ref	Expression
1		dedex.1	. 2
2		dedex.2	. 2
3	1, 2	keepel 4009	1

Syntax hints:  e.wcel 1818  cvv 3109  ifcif 3941

This theorem is referenced by:  ifexg  4011  opex  4716  fnoe  7179  oev  7183  unxpdomlem1  7744  unxpdomlem2  7745  unxpdomlem3  7746  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  iunfictbso  8516  fin23lem12  8732  axcc2lem  8837  ttukeylem3  8912  pwfseqlem2  9058  pwfseqlem3  9059  xnegex  11436  xaddval  11451  xmulval  11453  seqf1olem1  12146  expval  12168  bcval  12382  ccatlen  12594  ccatvalfn  12599  swrdval  12644  swrd00  12645  swrd0  12658  cshfn  12761  cshnz  12763  sgnval  12921  fsumser  13552  isumless  13657  rpnnen2lem1  13948  ruclem1  13964  sadcp1  14105  smupp1  14130  gcdval  14146  eucalgval2  14210  pcval  14368  pcmpt  14411  prmreclem2  14435  prmreclem5  14438  ramub1lem2  14545  ramcl  14547  acsfn  15056  gsumvalx  15897  mulgfval  16143  mulgval  16144  mulgfn  16145  odval  16558  odf  16561  gexval  16598  frgpup3lem  16795  dprdfeq0  17062  dprdfeq0OLD  17069  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  abvtrivd  17489  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mvrval2  18078  mplmonmul  18126  mplmon2  18158  coe1tmmul2fv  18319  coe1pwmulfv  18321  xrsdsval  18462  uvcvval  18817  mat1comp  18942  mat1ov  18950  matsc  18952  mat1dimid  18976  dmatmulcl  19002  scmatscmiddistr  19010  scmatscm  19015  mdetunilem9  19122  minmar1eval  19151  symgmatr01  19156  m2cpm  19242  m2cpminvid2lem  19255  decpmatid  19271  monmatcollpw  19280  mp2pm2mplem4  19310  chmatval  19330  chfacffsupp  19357  ptcmplem2  20553  ptcmplem3  20554  iccpnfhmeo  21445  xrhmeo  21446  phtpycc  21491  pcovalg  21512  pcohtpylem  21519  ovolunlem1a  21907  ovolunlem1  21908  ovolicc1  21927  ioorval  21983  mbfmax  22056  i1f1lem  22096  itg11  22098  itg1addlem3  22105  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfi1flim  22130  itg2uba  22150  itg2splitlem  22155  itg2monolem1  22157  itg2gt0  22167  itg2cnlem1  22168  i1fibl  22214  itgeqa  22220  itgcn  22249  ditgex  22256  dvexp3  22379  ply1nzb  22523  ig1pval  22573  elply2  22593  dvply1  22680  aareccl  22722  dvtaylp  22765  pserdvlem2  22823  abelthlem9  22835  logtayl  23041  cxpval  23045  leibpilem2  23272  leibpi  23273  vmaval  23387  vmaf  23393  muval  23406  prmorcht  23452  pclogsum  23490  dchrinvcl  23528  dchrptlem2  23540  bposlem5  23563  lgsval  23575  lgsfval  23576  lgsdir  23605  lgsdilem2  23606  lgsdi  23607  lgsne0  23608  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  padicval  23802  padicabv  23815  ostth1  23818  axlowdimlem15  24259  axlowdim  24264  clwlkisclwwlklem2a2  24780  gxval  25260  xrge0iifcv  27916  xrge0iifhom  27919  ddeval1  28206  ddeval0  28207  ofccat  28497  lgamgulmlem4  28574  lgamgulmlem5  28575  igamval  28589  mrsubcv  28870  mrsubrn  28873  dfrdg2  29228  mblfinlem2  30052  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  fdc  30238  flcidc  31123  lcmval  31198  fourierdlem29  31918  fourierdlem56  31945  fourierswlem  32013  fouriersw  32014  linc0scn0  33024  linc1  33026  lincext2  33056  renegclALT  34694  cdleme50f  36268  cdlemk40  36643  cdlemk56  36697  dihval  36959  dihf11lem  36993  mapdhval  37451  hdmap1vallem  37525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942