MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifex Structured version   Unicode version

Theorem ifex 3870
Description: Conditional operator existence. (Contributed by NM, 2-Sep-2004.)
Hypotheses
Ref Expression
dedex.1  |-  A  e. 
_V
dedex.2  |-  B  e. 
_V
Assertion
Ref Expression
ifex  |-  if (
ph ,  A ,  B )  e.  _V

Proof of Theorem ifex
StepHypRef Expression
1 dedex.1 . 2  |-  A  e. 
_V
2 dedex.2 . 2  |-  B  e. 
_V
31, 2keepel 3869 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2984   ifcif 3803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3804
This theorem is referenced by:  ifexg  3871  opex  4568  fnoe  6962  oev  6966  unxpdomlem1  7529  unxpdomlem2  7530  unxpdomlem3  7531  cantnflem1d  7908  cantnflem1  7909  cantnflem1dOLD  7931  cantnflem1OLD  7932  iunfictbso  8296  fin23lem12  8512  axcc2lem  8617  ttukeylem3  8692  pwfseqlem2  8838  pwfseqlem3  8839  xnegex  11190  xaddval  11205  xmulval  11207  seqf1olem1  11857  expval  11879  bcval  12092  ccatlen  12287  ccatvalfn  12292  swrdval  12325  swrd00  12326  swrd0  12339  cshfn  12439  cshnz  12441  sgnval  12589  fsumser  13219  isumless  13320  rpnnen2lem1  13509  ruclem1  13525  sadcp1  13663  smupp1  13688  gcdval  13704  eucalgval2  13768  pcval  13923  pcmpt  13966  prmreclem2  13990  prmreclem5  13993  ramub1lem2  14100  ramcl  14102  acsfn  14609  gsumvalx  15514  mulgfval  15640  mulgval  15641  mulgfn  15642  odval  16049  odf  16052  gexval  16089  frgpup3lem  16286  dprdfeq0  16524  dprdfeq0OLD  16531  dmdprdsplitlem  16546  dmdprdsplitlemOLD  16547  abvtrivd  16937  psrlidm  17486  psrlidmOLD  17487  psrridm  17488  psrridmOLD  17489  mvrval2  17507  mplmonmul  17555  mplmon2  17587  coe1tmmul2fv  17743  coe1pwmulfv  17745  xrsdsval  17869  uvcvval  18223  dmatcomp  18315  mat1ov  18347  matsc  18353  mdetunilem9  18438  minmar1eval  18467  symgmatr01  18472  ptcmplem2  19637  ptcmplem3  19638  iccpnfhmeo  20529  xrhmeo  20530  phtpycc  20575  pcovalg  20596  pcohtpylem  20603  ovolunlem1a  20991  ovolunlem1  20992  ovolicc1  21011  ioorval  21066  mbfmax  21139  i1f1lem  21179  itg11  21181  itg1addlem3  21188  i1fres  21195  itg1climres  21204  mbfi1fseqlem4  21208  mbfi1fseqlem6  21210  mbfi1flimlem  21212  mbfi1flim  21213  itg2uba  21233  itg2splitlem  21238  itg2monolem1  21240  itg2gt0  21250  itg2cnlem1  21251  i1fibl  21297  itgeqa  21303  itgcn  21332  ditgex  21339  dvexp3  21462  ply1nzb  21606  ig1pval  21656  elply2  21676  dvply1  21762  aareccl  21804  dvtaylp  21847  pserdvlem2  21905  abelthlem9  21917  logtayl  22117  cxpval  22121  leibpilem2  22348  leibpi  22349  vmaval  22463  vmaf  22469  muval  22482  prmorcht  22528  pclogsum  22566  dchrinvcl  22604  dchrptlem2  22616  bposlem5  22639  lgsval  22651  lgsfval  22652  lgsdir  22681  lgsdilem2  22682  lgsdi  22683  lgsne0  22684  pntrlog2bndlem4  22841  pntrlog2bndlem5  22842  padicval  22878  padicabv  22891  ostth1  22894  axlowdimlem15  23214  axlowdim  23219  gxval  23757  xrge0iifcv  26376  xrge0iifhom  26379  ddeval1  26662  ddeval0  26663  ofccat  26953  lgamgulmlem4  27030  lgamgulmlem5  27031  igamval  27045  dfrdg2  27621  mblfinlem2  28441  itg2addnclem  28455  itg2addnclem2  28456  itg2addnclem3  28457  itg2addnc  28458  ftc1anclem5  28483  ftc1anclem7  28485  ftc1anclem8  28486  ftc1anc  28487  fdc  28653  flcidc  29543  clwlkisclwwlklem2a2  30454  mat1dimid  30882  dmatmulcl  30891  scmatmulcl  30898  pmatcollpw1id  30911  mp2pm2mplem4  30931  linc0scn0  30969  linc1  30971  lincext2  31001  renegclALT  32626  cdleme50f  34198  cdlemk40  34573  cdlemk56  34627  dihval  34889  dihf11lem  34923  mapdhval  35381  hdmap1vallem  35455
  Copyright terms: Public domain W3C validator