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

Theorem ifex 3925
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 3924 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   _Vcvv 3034   ifcif 3857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-if 3858
This theorem is referenced by:  ifexg  3926  opex  4626  fnoe  7078  oev  7082  unxpdomlem1  7640  unxpdomlem2  7641  unxpdomlem3  7642  cantnflem1d  8020  cantnflem1  8021  cantnflem1dOLD  8043  cantnflem1OLD  8044  iunfictbso  8408  fin23lem12  8624  axcc2lem  8729  ttukeylem3  8804  pwfseqlem2  8948  pwfseqlem3  8949  xnegex  11328  xaddval  11343  xmulval  11345  seqf1olem1  12049  expval  12071  bcval  12284  ccatlen  12503  ccatvalfn  12508  swrdval  12553  swrd00  12554  swrd0  12570  cshfn  12672  cshnz  12674  sgnval  12923  fsumser  13554  isumless  13659  rpnnen2lem1  13950  ruclem1  13966  sadcp1  14107  smupp1  14132  gcdval  14148  eucalgval2  14212  pcval  14370  pcmpt  14413  prmreclem2  14437  prmreclem5  14440  ramub1lem2  14547  ramcl  14549  acsfn  15066  gsumvalx  16014  mulgfval  16260  mulgval  16261  mulgfn  16262  odval  16675  odf  16678  gexval  16715  frgpup3lem  16912  dprdfeq0  17175  dprdfeq0OLD  17182  dmdprdsplitlem  17197  dmdprdsplitlemOLD  17198  abvtrivd  17602  psrlidm  18169  psrlidmOLD  18170  psrridm  18171  psrridmOLD  18172  mvrval2  18191  mplmonmul  18239  mplmon2  18271  coe1tmmul2fv  18432  coe1pwmulfv  18434  xrsdsval  18575  uvcvval  18906  mat1comp  19027  mat1ov  19035  matsc  19037  mat1dimid  19061  dmatmulcl  19087  scmatscmiddistr  19095  scmatscm  19100  mdetunilem9  19207  minmar1eval  19236  symgmatr01  19241  m2cpm  19327  m2cpminvid2lem  19340  decpmatid  19356  monmatcollpw  19365  mp2pm2mplem4  19395  chmatval  19415  chfacffsupp  19442  ptcmplem2  20638  ptcmplem3  20639  iccpnfhmeo  21530  xrhmeo  21531  phtpycc  21576  pcovalg  21597  pcohtpylem  21604  ovolunlem1a  21992  ovolunlem1  21993  ovolicc1  22012  ioorval  22068  mbfmax  22141  i1f1lem  22181  itg11  22183  itg1addlem3  22190  i1fres  22197  itg1climres  22206  mbfi1fseqlem4  22210  mbfi1fseqlem6  22212  mbfi1flimlem  22214  mbfi1flim  22215  itg2uba  22235  itg2splitlem  22240  itg2monolem1  22242  itg2gt0  22252  itg2cnlem1  22253  i1fibl  22299  itgeqa  22305  itgcn  22334  ditgex  22341  dvexp3  22464  ply1nzb  22608  ig1pval  22658  elply2  22678  dvply1  22765  aareccl  22807  dvtaylp  22850  pserdvlem2  22908  abelthlem9  22920  logtayl  23128  cxpval  23132  leibpilem2  23388  leibpi  23389  vmaval  23504  vmaf  23510  muval  23523  prmorcht  23569  pclogsum  23607  dchrinvcl  23645  dchrptlem2  23657  bposlem5  23680  lgsval  23692  lgsfval  23693  lgsdir  23722  lgsdilem2  23723  lgsdi  23724  lgsne0  23725  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  padicval  23919  padicabv  23932  ostth1  23935  axlowdimlem15  24380  axlowdim  24385  clwlkisclwwlklem2a2  24901  gxval  25377  xrge0iifcv  28070  xrge0iifhom  28073  ddeval1  28362  ddeval0  28363  ofccat  28680  lgamgulmlem4  28763  lgamgulmlem5  28764  igamval  28778  mrsubcv  29059  mrsubrn  29062  dfrdg2  29393  mblfinlem2  30217  itg2addnclem  30232  itg2addnclem2  30233  itg2addnclem3  30234  itg2addnc  30235  ftc1anclem5  30260  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  fdc  30404  flcidc  31291  lcmval  31366  fourierdlem29  32084  fourierdlem56  32111  fourierswlem  32179  fouriersw  32180  linc0scn0  33224  linc1  33226  lincext2  33256  blenval  33392  renegclALT  35107  cdleme50f  36681  cdlemk40  37056  cdlemk56  37110  dihval  37372  dihf11lem  37406  mapdhval  37864  hdmap1vallem  37938
  Copyright terms: Public domain W3C validator