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

Theorem ifex 3855
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 3854 1  |-  if (
ph ,  A ,  B )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   _Vcvv 2970   ifcif 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-if 3789
This theorem is referenced by:  ifexg  3856  opex  4553  fnoe  6946  oev  6950  unxpdomlem1  7513  unxpdomlem2  7514  unxpdomlem3  7515  cantnflem1d  7892  cantnflem1  7893  cantnflem1dOLD  7915  cantnflem1OLD  7916  iunfictbso  8280  fin23lem12  8496  axcc2lem  8601  ttukeylem3  8676  pwfseqlem2  8822  pwfseqlem3  8823  xnegex  11174  xaddval  11189  xmulval  11191  seqf1olem1  11841  expval  11863  bcval  12076  ccatlen  12271  ccatvalfn  12276  swrdval  12309  swrd00  12310  swrd0  12323  cshfn  12423  cshnz  12425  sgnval  12573  fsumser  13203  isumless  13304  rpnnen2lem1  13493  ruclem1  13509  sadcp1  13647  smupp1  13672  gcdval  13688  eucalgval2  13752  pcval  13907  pcmpt  13950  prmreclem2  13974  prmreclem5  13977  ramub1lem2  14084  ramcl  14086  acsfn  14593  gsumvalx  15497  mulgfval  15621  mulgval  15622  mulgfn  15623  odval  16030  odf  16033  gexval  16070  frgpup3lem  16267  dprdfeq0  16502  dprdfeq0OLD  16509  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  abvtrivd  16905  psrlidm  17464  psrlidmOLD  17465  psrridm  17466  psrridmOLD  17467  mvrval2  17485  mplmonmul  17533  mplmon2  17563  coe1tmmul2fv  17685  coe1pwmulfv  17687  xrsdsval  17757  uvcvval  18111  dmatcomp  18203  mat1ov  18235  matsc  18241  mdetunilem9  18326  minmar1eval  18355  symgmatr01  18360  ptcmplem2  19525  ptcmplem3  19526  iccpnfhmeo  20417  xrhmeo  20418  phtpycc  20463  pcovalg  20484  pcohtpylem  20491  ovolunlem1a  20879  ovolunlem1  20880  ovolicc1  20899  ioorval  20954  mbfmax  21027  i1f1lem  21067  itg11  21069  itg1addlem3  21076  i1fres  21083  itg1climres  21092  mbfi1fseqlem4  21096  mbfi1fseqlem6  21098  mbfi1flimlem  21100  mbfi1flim  21101  itg2uba  21121  itg2splitlem  21126  itg2monolem1  21128  itg2gt0  21138  itg2cnlem1  21139  i1fibl  21185  itgeqa  21191  itgcn  21220  ditgex  21227  dvexp3  21350  ply1nzb  21537  ig1pval  21587  elply2  21607  dvply1  21693  aareccl  21735  dvtaylp  21778  pserdvlem2  21836  abelthlem9  21848  logtayl  22048  cxpval  22052  leibpilem2  22279  leibpi  22280  vmaval  22394  vmaf  22400  muval  22413  prmorcht  22459  pclogsum  22497  dchrinvcl  22535  dchrptlem2  22547  bposlem5  22570  lgsval  22582  lgsfval  22583  lgsdir  22612  lgsdilem2  22613  lgsdi  22614  lgsne0  22615  pntrlog2bndlem4  22772  pntrlog2bndlem5  22773  padicval  22809  padicabv  22822  ostth1  22825  axlowdimlem15  23121  axlowdim  23126  gxval  23664  xrge0iifcv  26284  xrge0iifhom  26287  ddeval1  26570  ddeval0  26571  ofccat  26855  lgamgulmlem4  26932  lgamgulmlem5  26933  igamval  26947  dfrdg2  27522  mblfinlem2  28338  itg2addnclem  28352  itg2addnclem2  28353  itg2addnclem3  28354  itg2addnc  28355  ftc1anclem5  28380  ftc1anclem7  28382  ftc1anclem8  28383  ftc1anc  28384  fdc  28550  flcidc  29440  clwlkisclwwlklem2a2  30351  mat1dimid  30736  dmatmulcl  30745  scmatmulcl  30752  linc0scn0  30781  linc1  30783  lincext2  30813  renegclALT  32302  cdleme50f  33874  cdlemk40  34249  cdlemk56  34303  dihval  34565  dihf11lem  34599  mapdhval  35057  hdmap1vallem  35131
  Copyright terms: Public domain W3C validator