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

Theorem iffalse 3738
Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
iffalse  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )

Proof of Theorem iffalse
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dedlemb 922 . . 3  |-  ( -. 
ph  ->  ( x  e.  B  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 2550 . 2  |-  ( -. 
ph  ->  B  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3732 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2486 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358    /\ wa 359    = wceq 1652    e. wcel 1725   {cab 2421   ifcif 3731
This theorem is referenced by:  ifnefalse  3739  ifsb  3740  ifbi  3748  ifeq1da  3756  ifclda  3758  elimif  3760  ifbothda  3761  ifid  3763  ifeqor  3768  ifnot  3769  ifan  3770  ifor  3771  elimhyp  3779  elimhyp2v  3780  elimhyp3v  3781  elimhyp4v  3782  elimdhyp  3784  keephyp2v  3786  keephyp3v  3787  dfopif  3973  opprc  3997  somin1  5262  somincom  5263  dfiota4  5438  elimdelov  6145  riotav  6546  riotaund  6578  tz7.44-2  6657  tz7.44-3  6658  oevn0  6751  pw2f1olem  7204  unxpdomlem2  7306  unxpdomlem3  7307  oi0  7489  wemaplem2  7508  unwdomg  7544  ixpiunwdom  7551  cantnfp1lem1  7626  cantnfp1lem3  7628  cantnflem1d  7636  cantnflem1  7637  dfac12lem2  8016  fin23lem14  8205  axcc2lem  8308  ttukeylem5  8385  ttukeylem7  8387  canthp1lem2  8520  pwfseqlem3  8527  uzin  10510  xrmax1  10755  xrmax2  10756  xrmin1  10757  xrmin2  10758  max1ALT  10766  ifle  10775  xmulneg1  10840  rexmul  10842  xmulpnf1  10845  fzprval  11098  seqf1olem1  11354  seqf1olem2  11355  expnnval  11377  expneg  11381  bcval3  11589  ccatval2  11738  ccatco  11796  absmax  12125  sumeq2ii  12479  sumrblem  12497  fsumcvg  12498  summolem2a  12501  zsum  12504  sum0  12507  sumss  12510  sumss2  12512  fsumcvg2  12513  fsumsplit  12525  sumsplit  12544  ef0lem  12673  rpnnen2lem9  12814  ruclem2  12823  ruclem3  12824  sadadd2lem2  12954  sadcp1  12959  sadcaddlem  12961  sadadd2  12964  gcdn0val  13002  eucalgf  13066  eucalginv  13067  eucalglt  13068  iserodd  13201  pcgcd  13243  pcmptcl  13252  pcmpt  13253  pcmpt2  13254  pcprod  13256  fldivp1  13258  prmreclem2  13277  prmreclem4  13279  vdwlem6  13346  ramtub  13372  ressval2  13510  xpsaddlem  13792  xpsvsca  13796  setcepi  14235  gsumval2a  14774  mulgnn  14888  mulgnegnn  14892  odlem2  15169  dfod2  15192  gsumval3a  15504  gsumzsplit  15521  dmdprdsplitlem  15587  abvtrivd  15920  psrlidm  16459  psrridm  16460  mvridlem  16475  mvrf1  16481  mvrcl  16504  mplmon  16518  mplmonmul  16519  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  mplmon2  16545  psrbagsn  16547  coe1tmfv2  16659  obselocv  16947  ptpjpre1  17595  ptpjpre2  17604  ptbasfi  17605  ptopn2  17608  xkopt  17679  isfcls  18033  ptcmplem2  18076  ptcmplem3  18077  tsmssplit  18173  dscmet  18612  dscopn  18613  xrsxmet  18832  icccmplem2  18846  cnmpt2pc  18945  iccpnfcnv  18961  xrhmeo  18963  htpycc  18997  pco1  19032  pcoval2  19033  pcohtpylem  19036  pcopt  19039  pcopt2  19040  pcoass  19041  pcorevlem  19043  ovolunlem1a  19384  ovolunlem1  19385  ovolicc1  19404  i1f1lem  19573  itg11  19575  itg1addlem2  19581  itg1addlem3  19582  i1fres  19589  itg1climres  19598  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  mbfi1flim  19607  itg2const2  19625  itg2seq  19626  itg2uba  19627  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2gt0  19644  itg2cnlem1  19645  itg2cnlem2  19646  itgeq2  19661  itg0  19663  iblss  19688  iblss2  19689  itgle  19693  itgss  19695  itgss2  19696  itgss3  19698  itgless  19700  ibladdlem  19703  itgaddlem1  19706  iblabslem  19711  iblabs  19712  iblabsr  19713  iblmulc2  19714  bddmulibl  19722  itggt0  19725  itgcn  19726  ditgneg  19736  limccnp2  19771  dvexp2  19832  lhop2  19891  evlslem3  19927  evlslem1  19928  deg1add  20018  ig1pval3  20089  elply2  20107  ply1termlem  20114  plyeq0lem  20121  plypf1  20123  coeeq2  20153  dgrle  20154  coe1termlem  20168  dvply1  20193  vieta1lem2  20220  pserdvlem2  20336  abelthlem9  20348  logcnlem3  20527  logtayllem  20542  logtayl  20543  cxpef  20548  rlimcnp2  20797  efrlim  20800  isppw  20889  isnsqf  20910  mule1  20923  sqff1o  20957  muinv  20970  chtublem  20987  dchrelbasd  21015  bposlem1  21060  bposlem3  21062  bposlem5  21064  bposlem6  21065  lgsval2lem  21082  lgsval4  21092  lgsval4a  21094  lgsneg  21095  lgsneg1  21096  lgsdilem  21098  lgsdir2  21104  lgsdir  21106  lgsdi  21108  lgsne0  21109  rplogsumlem2  21171  dchrvmasum2if  21183  dchrisum0fno1  21197  rplogsum  21213  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  padicabv  21316  ostth1  21319  ostth2lem4  21322  ostth3  21324  gxpval  21839  gxnval  21840  ifbieq12d2  23994  elimifd  23996  elim2if  23997  imadifxp  24030  partfun  24079  xrge0iifcnv  24311  xrge0iifcv  24312  xrge0iif1  24316  indval2  24404  ind0  24409  esumpinfval  24455  sigaclfu2  24496  ballotlemrv2  24771  igamgam  24825  prodeq2ii  25231  prodrblem  25247  fprodcvg  25248  prodmolem2a  25252  zprod  25255  fprodntriv  25260  prod0  25261  prodss  25265  fprodsplit  25281  dfrdg2  25415  dfrdg3  25416  unisnif  25762  dfrdg4  25787  axlowdimlem15  25887  axlowdim  25892  mblfinlem  26234  mbfposadd  26244  itg2addnclem  26246  itg2addnclem2  26247  itg2addnclem3  26248  itg2gt0cn  26250  ibladdnclem  26251  itgaddnclem1  26253  iblabsnclem  26258  iblabsnc  26259  iblmulc2nc  26260  bddiblnc  26265  areacirclem6  26277  areacirc  26278  fdc  26430  heiborlem4  26504  heiborlem6  26506  pw2f1ocnv  27089  aomclem5  27114  kelac1  27119  uvcvv0  27197  uvcff  27198  flcidc  27337  pmtrmvd  27356  mamulid  27416  mamurid  27417  refsum2cnlem1  27665  afvnfundmuv  27960  ifeqda  28032  2if2  28033  modifeq2int  28129  swrdnd  28144  swrd0  28145  swrdvalodm2  28150  swrdvalodm  28151  swrdccatin2  28166  swrdccat  28172  swrdccat3a  28173  swrdccat3b  28175  cshwidxm  28202  cshwidxn  28203  2cshw  28212  2cshwcom  28220  ifnmfalse  28433  sgnp  28447  sgnn  28451  cdleme27a  31091  cdleme31sn2  31113  cdleme31fv2  31117  cdlemefr27cl  31127  dihvalc  31958  mapdhval2  32451  hdmap1val2  32526
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