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

Theorem ifex 3961
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 3960 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   _Vcvv 3057   ifcif 3893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-if 3894
This theorem is referenced by:  ifexg  3962  opex  4678  fnoe  7238  oev  7242  unxpdomlem1  7802  unxpdomlem2  7803  unxpdomlem3  7804  cantnflem1d  8219  cantnflem1  8220  iunfictbso  8571  fin23lem12  8787  axcc2lem  8892  ttukeylem3  8967  pwfseqlem2  9110  pwfseqlem3  9111  xnegex  11530  xaddval  11545  xmulval  11547  seqf1olem1  12284  expval  12306  bcval  12521  ccatlen  12757  ccatvalfn  12762  swrdval  12810  swrd00  12811  swrd0  12827  cshfn  12929  cshnz  12931  sgnval  13200  fsumser  13845  isumless  13952  rpnnen2lem1  14316  ruclem1  14332  sadcp1  14478  smupp1  14503  gcdval  14519  eucalgval2  14589  lcmval  14604  lcmvalOLD  14605  pcval  14843  pcmpt  14886  prmreclem2  14910  prmreclem5  14913  ramub1lem2  15034  ramcl  15036  acsfn  15614  gsumvalx  16562  mulgfval  16808  mulgval  16809  mulgfn  16810  odval  17229  odvalOLD  17232  odf  17235  odfOLD  17251  gexval  17276  gexvalOLD  17278  frgpup3lem  17476  dprdfeq0  17704  dmdprdsplitlem  17719  abvtrivd  18117  psrlidm  18676  psrridm  18677  mvrval2  18695  mplmonmul  18737  mplmon2  18765  coe1tmmul2fv  18920  coe1pwmulfv  18922  xrsdsval  19061  uvcvval  19393  mat1comp  19514  mat1ov  19522  matsc  19524  mat1dimid  19548  dmatmulcl  19574  scmatscmiddistr  19582  scmatscm  19587  mdetunilem9  19694  minmar1eval  19723  symgmatr01  19728  m2cpm  19814  m2cpminvid2lem  19827  decpmatid  19843  monmatcollpw  19852  mp2pm2mplem4  19882  chmatval  19902  chfacffsupp  19929  ptcmplem2  21117  ptcmplem3  21118  iccpnfhmeo  22022  xrhmeo  22023  phtpycc  22071  pcovalg  22092  pcohtpylem  22099  ovolunlem1a  22498  ovolunlem1  22499  ovolicc1  22518  ioorval  22575  ioorvalOLD  22580  mbfmax  22654  i1f1lem  22696  itg11  22698  itg1addlem3  22705  i1fres  22712  itg1climres  22721  mbfi1fseqlem4  22725  mbfi1fseqlem6  22727  mbfi1flimlem  22729  mbfi1flim  22730  itg2uba  22750  itg2splitlem  22755  itg2monolem1  22757  itg2gt0  22767  itg2cnlem1  22768  i1fibl  22814  itgeqa  22820  itgcn  22849  ditgex  22856  dvexp3  22979  ply1nzb  23120  ig1pval  23173  ig1pvalOLD  23179  elply2  23199  dvply1  23286  aareccl  23331  dvtaylp  23374  pserdvlem2  23432  abelthlem9  23444  logtayl  23654  cxpval  23658  leibpilem2  23916  leibpi  23917  lgamgulmlem4  24006  lgamgulmlem5  24007  igamval  24021  vmaval  24089  vmaf  24095  muval  24108  prmorcht  24154  pclogsum  24192  dchrinvcl  24230  dchrptlem2  24242  bposlem5  24265  lgsval  24277  lgsfval  24278  lgsdir  24307  lgsdilem2  24308  lgsdi  24309  lgsne0  24310  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  padicval  24504  padicabv  24517  ostth1  24520  axlowdimlem15  25035  axlowdim  25040  clwlkisclwwlklem2a2  25557  gxval  26035  psgnfzto1stlem  28662  xrge0iifcv  28789  xrge0iifhom  28792  ddeval1  29106  ddeval0  29107  ofccat  29478  mrsubcv  30197  mrsubrn  30200  dfrdg2  30491  finxpreclem2  31827  finxpreclem5  31832  poimirlem2  31987  poimirlem24  32009  mblfinlem2  32023  itg2addnclem  32038  itg2addnclem2  32039  itg2addnclem3  32040  itg2addnc  32041  ftc1anclem5  32066  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  fdc  32119  renegclALT  32580  cdleme50f  34154  cdlemk40  34529  cdlemk56  34583  dihval  34845  dihf11lem  34879  mapdhval  35337  hdmap1vallem  35411  flcidc  36085  fourierdlem29  38036  fourierdlem56  38064  fourierswlem  38132  fouriersw  38133  nnfoctbdjlem  38331  isomenndlem  38389  hoidmvval  38437  hspmbl  38489  vtxval  39151  iedgval  39152  linc0scn0  40489  linc1  40491  lincext2  40521  blenval  40655
  Copyright terms: Public domain W3C validator