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

Theorem iffalse 3574
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 )
Dummy variable  x is distinct from all other variables.

Proof of Theorem iffalse
StepHypRef Expression
1 dedlemb 923 . . 3  |-  ( -. 
ph  ->  ( x  e.  B  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 2400 . 2  |-  ( -. 
ph  ->  B  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3568 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2336 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359    /\ wa 360    = wceq 1624    e. wcel 1685   {cab 2271   ifcif 3567
This theorem is referenced by:  ifnefalse  3575  ifsb  3576  ifbi  3584  ifeq1da  3592  ifclda  3594  elimif  3596  ifbothda  3597  ifid  3599  ifeqor  3604  ifnot  3605  ifan  3606  ifor  3607  elimhyp  3615  elimhyp2v  3616  elimhyp3v  3617  elimhyp4v  3618  elimdhyp  3620  keephyp2v  3622  keephyp3v  3623  dfopif  3795  opprc  3819  somin1  5079  somincom  5080  elimdelov  5889  riotav  6305  riotaund  6337  tz7.44-2  6416  tz7.44-3  6417  oevn0  6510  pw2f1olem  6962  unxpdomlem2  7064  unxpdomlem3  7065  oi0  7239  wemaplem2  7258  unwdomg  7294  ixpiunwdom  7301  cantnfp1lem1  7376  cantnfp1lem3  7378  cantnflem1d  7386  cantnflem1  7387  dfac12lem2  7766  fin23lem14  7955  axcc2lem  8058  ttukeylem5  8136  ttukeylem7  8138  canthp1lem2  8271  pwfseqlem3  8278  uzin  10256  xrmax1  10499  xrmax2  10500  xrmin1  10501  xrmin2  10502  max1ALT  10510  ifle  10519  xmulneg1  10584  rexmul  10586  xmulpnf1  10589  fzprval  10839  seqf1olem1  11080  seqf1olem2  11081  expnnval  11102  expneg  11106  bcval3  11314  ccatval2  11427  ccatco  11485  absmax  11808  sumeq2ii  12161  sumrblem  12179  fsumcvg  12180  summolem2a  12183  zsum  12186  sum0  12189  sumss  12192  sumss2  12194  fsumcvg2  12195  fsumsplit  12207  sumsplit  12226  ef0lem  12355  rpnnen2lem9  12496  ruclem2  12505  ruclem3  12506  sadadd2lem2  12636  sadcp1  12641  sadcaddlem  12643  sadadd2  12646  gcdn0val  12684  eucalgf  12748  eucalginv  12749  eucalglt  12750  iserodd  12883  pcgcd  12925  pcmptcl  12934  pcmpt  12935  pcmpt2  12936  pcprod  12938  fldivp1  12940  prmreclem2  12959  prmreclem4  12961  vdwlem6  13028  ramtub  13054  ressval2  13192  xpsaddlem  13472  xpsvsca  13476  setcepi  13915  gsumval2a  14454  mulgnn  14568  mulgnegnn  14572  odlem2  14849  dfod2  14872  gsumval3a  15184  gsumzsplit  15201  dmdprdsplitlem  15267  abvtrivd  15600  psrlidm  16143  psrridm  16144  mvridlem  16159  mvrf1  16165  mvrcl  16188  mplmon  16202  mplmonmul  16203  mplcoe1  16204  mplcoe3  16205  mplcoe2  16206  mplmon2  16229  psrbagsn  16231  coe1tmfv2  16346  obselocv  16623  ptpjpre1  17261  ptpjpre2  17270  ptbasfi  17271  ptopn2  17274  xkopt  17344  isfcls  17699  ptcmplem2  17742  ptcmplem3  17743  tsmssplit  17829  dscmet  18090  dscopn  18091  xrsxmet  18310  icccmplem2  18323  cnmpt2pc  18421  iccpnfcnv  18437  xrhmeo  18439  htpycc  18473  pco1  18508  pcoval2  18509  pcohtpylem  18512  pcopt  18515  pcopt2  18516  pcoass  18517  pcorevlem  18519  ovolunlem1a  18850  ovolunlem1  18851  ovolicc1  18870  i1f1lem  19039  itg11  19041  itg1addlem2  19047  itg1addlem3  19048  i1fres  19055  itg1climres  19064  mbfi1fseqlem4  19068  mbfi1fseqlem5  19069  mbfi1flim  19073  itg2const2  19091  itg2seq  19092  itg2uba  19093  itg2splitlem  19098  itg2split  19099  itg2monolem1  19100  itg2gt0  19110  itg2cnlem1  19111  itg2cnlem2  19112  itgeq2  19127  itg0  19129  iblss  19154  iblss2  19155  itgle  19159  itgss  19161  itgss2  19162  itgss3  19164  itgless  19166  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  bddmulibl  19188  itggt0  19191  itgcn  19192  ditgneg  19202  limccnp2  19237  dvexp2  19298  lhop2  19357  evlslem3  19393  evlslem1  19394  deg1add  19484  ig1pval3  19555  elply2  19573  ply1termlem  19580  plyeq0lem  19587  plypf1  19589  coeeq2  19619  dgrle  19620  coe1termlem  19634  dvply1  19659  vieta1lem2  19686  pserdvlem2  19799  abelthlem9  19811  logcnlem3  19986  logtayllem  20001  logtayl  20002  cxpef  20007  rlimcnp2  20256  efrlim  20259  isppw  20347  isnsqf  20368  mule1  20381  sqff1o  20415  muinv  20428  chtublem  20445  dchrelbasd  20473  bposlem1  20518  bposlem3  20520  bposlem5  20522  bposlem6  20523  lgsval2lem  20540  lgsval4  20550  lgsval4a  20552  lgsneg  20553  lgsneg1  20554  lgsdilem  20556  lgsdir2  20562  lgsdir  20564  lgsdi  20566  lgsne0  20567  rplogsumlem2  20629  dchrvmasum2if  20641  dchrisum0fno1  20655  rplogsum  20671  pntrlog2bndlem4  20724  pntrlog2bndlem5  20725  padicabv  20774  ostth1  20777  ostth2lem4  20780  ostth3  20782  gxpval  20919  gxnval  20920  ballotlemrv2  23074  dfrdg2  23554  dfrdg3  23555  unisnif  23872  dfrdg4  23896  axlowdimlem15  23992  axlowdim  23997  repcpwti  24561  dffprod  24719  isconc2  25407  lineval3a  25483  sgplpte22  25538  isray2  25553  fdc  25855  heiborlem4  25938  heiborlem6  25940  pw2f1ocnv  26530  aomclem5  26555  kelac1  26561  uvcvv0  26639  uvcff  26640  flcidc  26779  pmtrmvd  26798  mamulid  26858  mamurid  26859  refsum2cnlem1  27108  afvnfundmuv  27382  ifnmfalse  27494  sgnp  27508  sgnn  27512  cdleme27a  29824  cdleme31sn2  29846  cdleme31fv2  29850  cdlemefr27cl  29860  dihvalc  30691  mapdhval2  31184  hdmap1val2  31259
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-if 3568
  Copyright terms: Public domain W3C validator