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

Theorem ifex 3979
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 3978 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869   _Vcvv 3082   ifcif 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-if 3912
This theorem is referenced by:  ifexg  3980  opex  4684  fnoe  7222  oev  7226  unxpdomlem1  7784  unxpdomlem2  7785  unxpdomlem3  7786  cantnflem1d  8200  cantnflem1  8201  iunfictbso  8551  fin23lem12  8767  axcc2lem  8872  ttukeylem3  8947  pwfseqlem2  9090  pwfseqlem3  9091  xnegex  11507  xaddval  11522  xmulval  11524  seqf1olem1  12257  expval  12279  bcval  12494  ccatlen  12723  ccatvalfn  12728  swrdval  12773  swrd00  12774  swrd0  12790  cshfn  12892  cshnz  12894  sgnval  13149  fsumser  13793  isumless  13900  rpnnen2lem1  14264  ruclem1  14280  sadcp1  14426  smupp1  14451  gcdval  14467  eucalgval2  14537  lcmval  14552  lcmvalOLD  14553  pcval  14791  pcmpt  14834  prmreclem2  14858  prmreclem5  14861  ramub1lem2  14982  ramcl  14984  acsfn  15562  gsumvalx  16510  mulgfval  16756  mulgval  16757  mulgfn  16758  odval  17177  odvalOLD  17180  odf  17183  odfOLD  17199  gexval  17224  gexvalOLD  17226  frgpup3lem  17424  dprdfeq0  17652  dmdprdsplitlem  17667  abvtrivd  18065  psrlidm  18624  psrridm  18625  mvrval2  18643  mplmonmul  18685  mplmon2  18713  coe1tmmul2fv  18868  coe1pwmulfv  18870  xrsdsval  19009  uvcvval  19340  mat1comp  19461  mat1ov  19469  matsc  19471  mat1dimid  19495  dmatmulcl  19521  scmatscmiddistr  19529  scmatscm  19534  mdetunilem9  19641  minmar1eval  19670  symgmatr01  19675  m2cpm  19761  m2cpminvid2lem  19774  decpmatid  19790  monmatcollpw  19799  mp2pm2mplem4  19829  chmatval  19849  chfacffsupp  19876  ptcmplem2  21064  ptcmplem3  21065  iccpnfhmeo  21969  xrhmeo  21970  phtpycc  22018  pcovalg  22039  pcohtpylem  22046  ovolunlem1a  22445  ovolunlem1  22446  ovolicc1  22465  ioorval  22522  ioorvalOLD  22527  mbfmax  22601  i1f1lem  22643  itg11  22645  itg1addlem3  22652  i1fres  22659  itg1climres  22668  mbfi1fseqlem4  22672  mbfi1fseqlem6  22674  mbfi1flimlem  22676  mbfi1flim  22677  itg2uba  22697  itg2splitlem  22702  itg2monolem1  22704  itg2gt0  22714  itg2cnlem1  22715  i1fibl  22761  itgeqa  22767  itgcn  22796  ditgex  22803  dvexp3  22926  ply1nzb  23067  ig1pval  23120  ig1pvalOLD  23126  elply2  23146  dvply1  23233  aareccl  23278  dvtaylp  23321  pserdvlem2  23379  abelthlem9  23391  logtayl  23601  cxpval  23605  leibpilem2  23863  leibpi  23864  lgamgulmlem4  23953  lgamgulmlem5  23954  igamval  23968  vmaval  24036  vmaf  24042  muval  24055  prmorcht  24101  pclogsum  24139  dchrinvcl  24177  dchrptlem2  24189  bposlem5  24212  lgsval  24224  lgsfval  24225  lgsdir  24254  lgsdilem2  24255  lgsdi  24256  lgsne0  24257  pntrlog2bndlem4  24414  pntrlog2bndlem5  24415  padicval  24451  padicabv  24464  ostth1  24467  axlowdimlem15  24982  axlowdim  24987  clwlkisclwwlklem2a2  25504  gxval  25982  psgnfzto1stlem  28619  xrge0iifcv  28746  xrge0iifhom  28749  ddeval1  29063  ddeval0  29064  ofccat  29435  mrsubcv  30154  mrsubrn  30157  dfrdg2  30447  finxpreclem2  31744  finxpreclem5  31749  poimirlem2  31904  poimirlem24  31926  mblfinlem2  31940  itg2addnclem  31955  itg2addnclem2  31956  itg2addnclem3  31957  itg2addnc  31958  ftc1anclem5  31983  ftc1anclem7  31985  ftc1anclem8  31986  ftc1anc  31987  fdc  32036  renegclALT  32502  cdleme50f  34076  cdlemk40  34451  cdlemk56  34505  dihval  34767  dihf11lem  34801  mapdhval  35259  hdmap1vallem  35333  flcidc  36008  fourierdlem29  37866  fourierdlem56  37894  fourierswlem  37962  fouriersw  37963  nnfoctbdjlem  38120  isomenndlem  38178  vtxval  38819  iedgval  38820  linc0scn0  39610  linc1  39612  lincext2  39642  blenval  39776
  Copyright terms: Public domain W3C validator