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

Theorem ifex 3623
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 3622 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   ifcif 3565
This theorem is referenced by:  ifexg  3624  opex  4237  riotaex  6308  fnoe  6509  oev  6513  unxpdomlem1  7067  unxpdomlem2  7068  unxpdomlem3  7069  cantnflem1d  7390  cantnflem1  7391  iunfictbso  7741  fin23lem12  7957  axcc2lem  8062  ttukeylem3  8138  pwfseqlem2  8281  pwfseqlem3  8282  xnegex  10535  xaddval  10550  xmulval  10552  seqf1olem1  11085  expval  11106  bcval  11317  ccatlen  11430  swrdval  11450  swrd00  11451  fsumser  12203  isumless  12304  rpnnen2lem1  12493  ruclem1  12509  sadcp1  12646  smupp1  12671  gcdval  12687  eucalgval2  12751  pcval  12897  pcmpt  12940  prmreclem2  12964  prmreclem5  12967  ramub1lem2  13074  ramcl  13076  acsfn  13561  gsumvalx  14451  mulgfval  14568  mulgval  14569  mulgfn  14570  odval  14849  odf  14852  gexval  14889  frgpup3lem  15086  dprdfeq0  15257  dmdprdsplitlem  15272  abvtrivd  15605  psrlidm  16148  psrridm  16149  mvrval2  16167  mplmonmul  16208  mplmon2  16234  coe1tmmul2fv  16354  coe1pwmulfv  16356  xrsdsval  16415  ptcmplem2  17747  ptcmplem3  17748  iccpnfhmeo  18443  xrhmeo  18444  phtpycc  18489  pcovalg  18510  pcohtpylem  18517  ovolunlem1a  18855  ovolunlem1  18856  ovolicc1  18875  ioorval  18929  mbfmax  19004  i1f1lem  19044  itg11  19046  itg1addlem3  19053  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfi1flim  19078  itg2uba  19098  itg2splitlem  19103  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  i1fibl  19162  itgeqa  19168  itgcn  19197  ditgex  19202  dvexp3  19325  ply1nzb  19508  ig1pval  19558  elply2  19578  dvply1  19664  aareccl  19706  dvtaylp  19749  pserdvlem2  19804  abelthlem9  19816  logtayl  20007  cxpval  20011  leibpilem2  20237  leibpi  20238  vmaval  20351  vmaf  20357  muval  20370  prmorcht  20416  pclogsum  20454  dchrinvcl  20492  dchrptlem2  20504  bposlem5  20527  lgsval  20539  lgsfval  20540  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  padicval  20766  padicabv  20779  ostth1  20782  gxval  20925  xrge0iifcv  23316  xrge0iifhom  23319  dfrdg2  24152  axlowdimlem15  24584  axlowdim  24589  prodex  25304  lineval222  26079  lineval3a  26083  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  fdc  26455  uvcvval  27235  flcidc  27379  mamulid  27458  mamurid  27459  sgnval  28245  cdleme50f  30731  cdlemk40  31106  cdlemk56  31160  dihval  31422  dihf11lem  31456  mapdhval  31914  hdmap1vallem  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator