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

Theorem ifex 3789
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 3788 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2948   ifcif 3731
This theorem is referenced by:  ifexg  3790  opex  4419  riotaex  6545  fnoe  6746  oev  6750  unxpdomlem1  7305  unxpdomlem2  7306  unxpdomlem3  7307  cantnflem1d  7636  cantnflem1  7637  iunfictbso  7987  fin23lem12  8203  axcc2lem  8308  ttukeylem3  8383  pwfseqlem2  8526  pwfseqlem3  8527  xnegex  10786  xaddval  10801  xmulval  10803  seqf1olem1  11354  expval  11376  bcval  11587  ccatlen  11736  swrdval  11756  swrd00  11757  fsumser  12516  isumless  12617  rpnnen2lem1  12806  ruclem1  12822  sadcp1  12959  smupp1  12984  gcdval  13000  eucalgval2  13064  pcval  13210  pcmpt  13253  prmreclem2  13277  prmreclem5  13280  ramub1lem2  13387  ramcl  13389  acsfn  13876  gsumvalx  14766  mulgfval  14883  mulgval  14884  mulgfn  14885  odval  15164  odf  15167  gexval  15204  frgpup3lem  15401  dprdfeq0  15572  dmdprdsplitlem  15587  abvtrivd  15920  psrlidm  16459  psrridm  16460  mvrval2  16478  mplmonmul  16519  mplmon2  16545  coe1tmmul2fv  16662  coe1pwmulfv  16664  xrsdsval  16734  ptcmplem2  18076  ptcmplem3  18077  iccpnfhmeo  18962  xrhmeo  18963  phtpycc  19008  pcovalg  19029  pcohtpylem  19036  ovolunlem1a  19384  ovolunlem1  19385  ovolicc1  19404  ioorval  19458  mbfmax  19533  i1f1lem  19573  itg11  19575  itg1addlem3  19582  i1fres  19589  itg1climres  19598  mbfi1fseqlem4  19602  mbfi1fseqlem6  19604  mbfi1flimlem  19606  mbfi1flim  19607  itg2uba  19627  itg2splitlem  19632  itg2monolem1  19634  itg2gt0  19644  itg2cnlem1  19645  i1fibl  19691  itgeqa  19697  itgcn  19726  ditgex  19731  dvexp3  19854  ply1nzb  20037  ig1pval  20087  elply2  20107  dvply1  20193  aareccl  20235  dvtaylp  20278  pserdvlem2  20336  abelthlem9  20348  logtayl  20543  cxpval  20547  leibpilem2  20773  leibpi  20774  vmaval  20888  vmaf  20894  muval  20907  prmorcht  20953  pclogsum  20991  dchrinvcl  21029  dchrptlem2  21041  bposlem5  21064  lgsval  21076  lgsfval  21077  lgsdir  21106  lgsdilem2  21107  lgsdi  21108  lgsne0  21109  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  padicval  21303  padicabv  21316  ostth1  21319  gxval  21838  xrge0iifcv  24312  xrge0iifhom  24315  lgamgulmlem4  24808  lgamgulmlem5  24809  igamval  24823  dfrdg2  25415  axlowdimlem15  25887  axlowdim  25892  mblfinlem  26234  itg2addnclem  26246  itg2addnclem2  26247  itg2addnclem3  26248  itg2addnc  26249  ftc1anclem5  26274  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  fdc  26440  uvcvval  27203  flcidc  27347  mamulid  27426  mamurid  27427  ccatvalfn  28151  sgnval  28455  cdleme50f  31276  cdlemk40  31651  cdlemk56  31705  dihval  31967  dihf11lem  32001  mapdhval  32459  hdmap1vallem  32533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator