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

Theorem ifex 4008
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 4007 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  ifexg  4009  opex  4711  fnoe  7160  oev  7164  unxpdomlem1  7724  unxpdomlem2  7725  unxpdomlem3  7726  cantnflem1d  8106  cantnflem1  8107  cantnflem1dOLD  8129  cantnflem1OLD  8130  iunfictbso  8494  fin23lem12  8710  axcc2lem  8815  ttukeylem3  8890  pwfseqlem2  9036  pwfseqlem3  9037  xnegex  11406  xaddval  11421  xmulval  11423  seqf1olem1  12113  expval  12135  bcval  12349  ccatlen  12558  ccatvalfn  12563  swrdval  12606  swrd00  12607  swrd0  12620  cshfn  12723  cshnz  12725  sgnval  12883  fsumser  13514  isumless  13619  rpnnen2lem1  13808  ruclem1  13824  sadcp1  13963  smupp1  13988  gcdval  14004  eucalgval2  14068  pcval  14226  pcmpt  14269  prmreclem2  14293  prmreclem5  14296  ramub1lem2  14403  ramcl  14405  acsfn  14913  gsumvalx  15821  mulgfval  15950  mulgval  15951  mulgfn  15952  odval  16361  odf  16364  gexval  16401  frgpup3lem  16598  dprdfeq0  16861  dprdfeq0OLD  16868  dmdprdsplitlem  16883  dmdprdsplitlemOLD  16884  abvtrivd  17284  psrlidm  17843  psrlidmOLD  17844  psrridm  17845  psrridmOLD  17846  mvrval2  17865  mplmonmul  17913  mplmon2  17945  coe1tmmul2fv  18106  coe1pwmulfv  18108  xrsdsval  18246  uvcvval  18600  mat1comp  18725  mat1ov  18733  matsc  18735  mat1dimid  18759  dmatmulcl  18785  scmatscmiddistr  18793  scmatscm  18798  mdetunilem9  18905  minmar1eval  18934  symgmatr01  18939  m2cpm  19025  m2cpminvid2lem  19038  decpmatid  19054  monmatcollpw  19063  mp2pm2mplem4  19093  chmatval  19113  chfacffsupp  19140  ptcmplem2  20304  ptcmplem3  20305  iccpnfhmeo  21196  xrhmeo  21197  phtpycc  21242  pcovalg  21263  pcohtpylem  21270  ovolunlem1a  21658  ovolunlem1  21659  ovolicc1  21678  ioorval  21734  mbfmax  21807  i1f1lem  21847  itg11  21849  itg1addlem3  21856  i1fres  21863  itg1climres  21872  mbfi1fseqlem4  21876  mbfi1fseqlem6  21878  mbfi1flimlem  21880  mbfi1flim  21881  itg2uba  21901  itg2splitlem  21906  itg2monolem1  21908  itg2gt0  21918  itg2cnlem1  21919  i1fibl  21965  itgeqa  21971  itgcn  22000  ditgex  22007  dvexp3  22130  ply1nzb  22274  ig1pval  22324  elply2  22344  dvply1  22430  aareccl  22472  dvtaylp  22515  pserdvlem2  22573  abelthlem9  22585  logtayl  22785  cxpval  22789  leibpilem2  23016  leibpi  23017  vmaval  23131  vmaf  23137  muval  23150  prmorcht  23196  pclogsum  23234  dchrinvcl  23272  dchrptlem2  23284  bposlem5  23307  lgsval  23319  lgsfval  23320  lgsdir  23349  lgsdilem2  23350  lgsdi  23351  lgsne0  23352  pntrlog2bndlem4  23509  pntrlog2bndlem5  23510  padicval  23546  padicabv  23559  ostth1  23562  axlowdimlem15  23951  axlowdim  23956  clwlkisclwwlklem2a2  24472  gxval  24952  xrge0iifcv  27568  xrge0iifhom  27571  ddeval1  27862  ddeval0  27863  ofccat  28153  lgamgulmlem4  28230  lgamgulmlem5  28231  igamval  28245  dfrdg2  28821  mblfinlem2  29645  itg2addnclem  29659  itg2addnclem2  29660  itg2addnclem3  29661  itg2addnc  29662  ftc1anclem5  29687  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  fdc  29857  flcidc  30744  lcmval  30814  fourierdlem29  31452  fourierdlem56  31479  fouriersw  31548  linc0scn0  32114  linc1  32116  lincext2  32146  renegclALT  33775  cdleme50f  35347  cdlemk40  35722  cdlemk56  35776  dihval  36038  dihf11lem  36072  mapdhval  36530  hdmap1vallem  36604
  Copyright terms: Public domain W3C validator