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

Theorem ifex 3995
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 3994 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   _Vcvv 3095   ifcif 3926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927
This theorem is referenced by:  ifexg  3996  opex  4701  fnoe  7162  oev  7166  unxpdomlem1  7726  unxpdomlem2  7727  unxpdomlem3  7728  cantnflem1d  8110  cantnflem1  8111  cantnflem1dOLD  8133  cantnflem1OLD  8134  iunfictbso  8498  fin23lem12  8714  axcc2lem  8819  ttukeylem3  8894  pwfseqlem2  9040  pwfseqlem3  9041  xnegex  11418  xaddval  11433  xmulval  11435  seqf1olem1  12128  expval  12150  bcval  12364  ccatlen  12576  ccatvalfn  12581  swrdval  12626  swrd00  12627  swrd0  12640  cshfn  12743  cshnz  12745  sgnval  12903  fsumser  13534  isumless  13639  rpnnen2lem1  13930  ruclem1  13946  sadcp1  14087  smupp1  14112  gcdval  14128  eucalgval2  14192  pcval  14350  pcmpt  14393  prmreclem2  14417  prmreclem5  14420  ramub1lem2  14527  ramcl  14529  acsfn  15038  gsumvalx  15876  mulgfval  16122  mulgval  16123  mulgfn  16124  odval  16537  odf  16540  gexval  16577  frgpup3lem  16774  dprdfeq0  17041  dprdfeq0OLD  17048  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  abvtrivd  17468  psrlidm  18035  psrlidmOLD  18036  psrridm  18037  psrridmOLD  18038  mvrval2  18057  mplmonmul  18105  mplmon2  18137  coe1tmmul2fv  18298  coe1pwmulfv  18300  xrsdsval  18441  uvcvval  18795  mat1comp  18920  mat1ov  18928  matsc  18930  mat1dimid  18954  dmatmulcl  18980  scmatscmiddistr  18988  scmatscm  18993  mdetunilem9  19100  minmar1eval  19129  symgmatr01  19134  m2cpm  19220  m2cpminvid2lem  19233  decpmatid  19249  monmatcollpw  19258  mp2pm2mplem4  19288  chmatval  19308  chfacffsupp  19335  ptcmplem2  20531  ptcmplem3  20532  iccpnfhmeo  21423  xrhmeo  21424  phtpycc  21469  pcovalg  21490  pcohtpylem  21497  ovolunlem1a  21885  ovolunlem1  21886  ovolicc1  21905  ioorval  21961  mbfmax  22034  i1f1lem  22074  itg11  22076  itg1addlem3  22083  i1fres  22090  itg1climres  22099  mbfi1fseqlem4  22103  mbfi1fseqlem6  22105  mbfi1flimlem  22107  mbfi1flim  22108  itg2uba  22128  itg2splitlem  22133  itg2monolem1  22135  itg2gt0  22145  itg2cnlem1  22146  i1fibl  22192  itgeqa  22198  itgcn  22227  ditgex  22234  dvexp3  22357  ply1nzb  22501  ig1pval  22551  elply2  22571  dvply1  22658  aareccl  22700  dvtaylp  22743  pserdvlem2  22801  abelthlem9  22813  logtayl  23019  cxpval  23023  leibpilem2  23250  leibpi  23251  vmaval  23365  vmaf  23371  muval  23384  prmorcht  23430  pclogsum  23468  dchrinvcl  23506  dchrptlem2  23518  bposlem5  23541  lgsval  23553  lgsfval  23554  lgsdir  23583  lgsdilem2  23584  lgsdi  23585  lgsne0  23586  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  padicval  23780  padicabv  23793  ostth1  23796  axlowdimlem15  24237  axlowdim  24242  clwlkisclwwlklem2a2  24758  gxval  25238  xrge0iifcv  27894  xrge0iifhom  27897  ddeval1  28184  ddeval0  28185  ofccat  28475  lgamgulmlem4  28552  lgamgulmlem5  28553  igamval  28567  mrsubcv  28848  mrsubrn  28851  dfrdg2  29204  mblfinlem2  30028  itg2addnclem  30042  itg2addnclem2  30043  itg2addnclem3  30044  itg2addnc  30045  ftc1anclem5  30070  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  fdc  30214  flcidc  31099  lcmval  31174  fourierdlem29  31872  fourierdlem56  31899  fourierswlem  31967  fouriersw  31968  linc0scn0  32894  linc1  32896  lincext2  32926  renegclALT  34569  cdleme50f  36143  cdlemk40  36518  cdlemk56  36572  dihval  36834  dihf11lem  36868  mapdhval  37326  hdmap1vallem  37400
  Copyright terms: Public domain W3C validator