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

Theorem ifex 3636
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 3635 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   ifcif 3578
This theorem is referenced by:  ifexg  3637  opex  4253  riotaex  6324  fnoe  6525  oev  6529  unxpdomlem1  7083  unxpdomlem2  7084  unxpdomlem3  7085  cantnflem1d  7406  cantnflem1  7407  iunfictbso  7757  fin23lem12  7973  axcc2lem  8078  ttukeylem3  8154  pwfseqlem2  8297  pwfseqlem3  8298  xnegex  10551  xaddval  10566  xmulval  10568  seqf1olem1  11101  expval  11122  bcval  11333  ccatlen  11446  swrdval  11466  swrd00  11467  fsumser  12219  isumless  12320  rpnnen2lem1  12509  ruclem1  12525  sadcp1  12662  smupp1  12687  gcdval  12703  eucalgval2  12767  pcval  12913  pcmpt  12956  prmreclem2  12980  prmreclem5  12983  ramub1lem2  13090  ramcl  13092  acsfn  13577  gsumvalx  14467  mulgfval  14584  mulgval  14585  mulgfn  14586  odval  14865  odf  14868  gexval  14905  frgpup3lem  15102  dprdfeq0  15273  dmdprdsplitlem  15288  abvtrivd  15621  psrlidm  16164  psrridm  16165  mvrval2  16183  mplmonmul  16224  mplmon2  16250  coe1tmmul2fv  16370  coe1pwmulfv  16372  xrsdsval  16431  ptcmplem2  17763  ptcmplem3  17764  iccpnfhmeo  18459  xrhmeo  18460  phtpycc  18505  pcovalg  18526  pcohtpylem  18533  ovolunlem1a  18871  ovolunlem1  18872  ovolicc1  18891  ioorval  18945  mbfmax  19020  i1f1lem  19060  itg11  19062  itg1addlem3  19069  i1fres  19076  itg1climres  19085  mbfi1fseqlem4  19089  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfi1flim  19094  itg2uba  19114  itg2splitlem  19119  itg2monolem1  19121  itg2gt0  19131  itg2cnlem1  19132  i1fibl  19178  itgeqa  19184  itgcn  19213  ditgex  19218  dvexp3  19341  ply1nzb  19524  ig1pval  19574  elply2  19594  dvply1  19680  aareccl  19722  dvtaylp  19765  pserdvlem2  19820  abelthlem9  19832  logtayl  20023  cxpval  20027  leibpilem2  20253  leibpi  20254  vmaval  20367  vmaf  20373  muval  20386  prmorcht  20432  pclogsum  20470  dchrinvcl  20508  dchrptlem2  20520  bposlem5  20543  lgsval  20555  lgsfval  20556  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  padicval  20782  padicabv  20795  ostth1  20798  gxval  20941  xrge0iifcv  23331  xrge0iifhom  23334  dfrdg2  24223  axlowdimlem15  24656  axlowdim  24661  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  prodex  25407  lineval222  26182  lineval3a  26186  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  fdc  26558  uvcvval  27338  flcidc  27482  mamulid  27561  mamurid  27562  sgnval  28499  cdleme50f  31353  cdlemk40  31728  cdlemk56  31782  dihval  32044  dihf11lem  32078  mapdhval  32536  hdmap1vallem  32610
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator