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

Theorem iffalse 4295
Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
iffalse 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalse
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dedlemb 1060 . . 3 𝜑 → (𝑥𝐵 ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))))
21abbi2dv 2933 . 2 𝜑𝐵 = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))})
3 df-if 4287 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐵 ∧ ¬ 𝜑))}
42, 3syl6reqr 2866 1 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 865   = wceq 1637  wcel 2157  {cab 2799  ifcif 4286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-if 4287
This theorem is referenced by:  iffalsei  4296  iffalsed  4297  ifnefalse  4298  ifsb  4299  ifbi  4307  ifeq1da  4316  ifeq12da  4318  ifclda  4320  ifeqda  4321  elimif  4322  ifbothda  4323  ifid  4325  ifnot  4336  ifan  4337  ifor  4338  2if2  4339  ifcomnan  4340  elimhyp  4349  elimhyp2v  4350  elimhyp3v  4351  elimhyp4v  4352  elimdhyp  4354  keephyp2v  4356  keephyp3v  4357  dfopif  4599  opprc  4625  somin1  5747  dfiota4OLD  6096  elimdelov  6969  ovif12  6972  oevn0  7835  pw2f1olem  8306  unxpdomlem2  8407  unxpdomlem3  8408  oi0  8675  wemaplem2  8694  ixpiunwdom  8738  cantnfp1lem3  8827  cantnflem1  8836  dfac12lem2  9254  fin23lem14  9443  axcc2lem  9546  ttukeylem5  9623  uzin  11941  xrmax1  12227  xrmax2  12228  xrmin1  12229  xrmin2  12230  max1ALT  12238  ifle  12249  xmulneg1  12320  modifeq2int  12959  seqf1olem1  13066  seqf1olem2  13067  bcval3  13316  swrdccat  13720  swrdccat3a  13721  swrdccat3b  13723  repswswrd  13758  cshword  13764  ccatco  13808  sumrblem  14668  fsumcvg  14669  summolem2a  14672  sumss  14681  fsumcvg2  14684  sumsplit  14725  prodeq2ii  14867  prodrblem  14883  fprodcvg  14884  prodmolem2a  14888  zprod  14891  prodss  14901  ruclem2  15184  ruclem3  15185  flodddiv4  15359  sadadd2lem2  15394  sadcp1  15399  sadcaddlem  15401  gcdn0val  15442  dfgcd2  15485  lcmn0val  15530  lcmfn0val  15558  pcgcd  15802  pcmptcl  15815  pcmpt  15816  pcmpt2  15817  pcprod  15819  fldivp1  15821  prmreclem2  15841  prmreclem4  15843  vdwlem6  15910  prmo1  15961  prmop1  15962  fvprmselelfz  15968  fvprmselgcd1  15969  ressval2  16143  xpsaddlem  16443  xpsvsca  16447  mreexexd  16516  setcepi  16945  pmtrmvd  18080  mvrf1  19637  mplcoe3  19678  mplmon2  19704  psrbagsn  19706  evlslem1  19726  obselocv  20286  dmatmul  20518  1mavmul  20569  mulmarep1gsum2  20595  1marepvmarrepid  20596  mdetdiag  20620  mdetrsca2  20625  mdetrlin2  20628  mdetunilem5  20637  mdetunilem7  20639  mdetunilem8  20640  mdetunilem9  20641  mndifsplit  20657  maducoeval2  20661  madugsum  20664  madurid  20665  smadiadetglem2  20694  1elcpmat  20737  decpmatid  20792  ptpjpre1  21592  ptbasfi  21602  isfcls  22030  ptcmplem2  22074  ptcmplem3  22075  dscmet  22594  dscopn  22595  icccmplem2  22843  cnmpt2pc  22944  iccpnfcnv  22960  xrhmeo  22962  pcoval2  23032  pcohtpylem  23035  pcopt  23038  pcopt2  23039  pcoass  23040  pcorevlem  23042  i1f1lem  23676  itg1addlem2  23684  itg1addlem3  23685  i1fres  23692  itg1climres  23701  mbfi1fseqlem4  23705  mbfi1fseqlem5  23706  itg2const2  23728  itg2seq  23729  itg2uba  23730  itg2splitlem  23735  itg2split  23736  itg2monolem1  23737  itg2gt0  23747  itg2cnlem1  23748  itg2cnlem2  23749  iblss  23791  iblss2  23792  itgle  23796  itgss  23798  ibladdlem  23806  itgaddlem1  23809  iblabslem  23814  iblabs  23815  iblabsr  23816  iblmulc2  23817  bddmulibl  23825  ditgneg  23841  elply2  24172  coeeq2  24218  dgrle  24219  coe1termlem  24234  logcnlem3  24610  igamgam  24995  isppw  25060  isnsqf  25081  mule1  25094  sqff1o  25128  chtublem  25156  dchrelbasd  25184  bposlem1  25229  bposlem3  25231  bposlem5  25233  bposlem6  25234  lgsneg  25266  lgsdilem  25269  lgsdir2  25275  lgsdir  25277  lgsdi  25279  lgsne0  25280  gausslemma2dlem1a  25310  2lgslem1c  25338  2lgs  25352  dchrvmasum2if  25406  ostth2lem4  25545  axlowdimlem15  26056  elimifd  29693  elim2if  29694  ifeq3da  29696  imadifxp  29745  resvval2  30160  pmtridf1o  30187  xrge0iifcnv  30310  indval2  30407  ddeval0  30629  eulerpartlemb  30761  plymulx0  30955  signsw0glem  30961  signswmnd  30965  dfrdg2  32026  dfrdg3  32027  noprefixmo  32174  nosupno  32175  nosupdm  32176  nosupbday  32177  nosupfv  32178  nosupres  32179  nosupbnd1lem1  32180  unisnif  32358  dfrdg4  32384  bj-xpima1sn  33255  finxpreclem2  33545  finxpreclem5  33550  matunitlindflem1  33720  poimirlem15  33739  poimirlem23  33747  mbfposadd  33771  itg2addnclem  33775  itg2addnclem3  33777  itg2gt0cn  33779  ibladdnclem  33780  itgaddnclem1  33782  iblabsnclem  33787  iblabsnc  33788  iblmulc2nc  33789  bddiblnc  33794  ftc1anclem5  33803  ftc1anclem7  33805  ftc1anclem8  33806  ftc1anc  33807  areacirclem5  33818  areacirc  33819  heiborlem4  33926  ac6s6  34292  riotaclbgBAD  34735  cdleme27a  36149  cdleme31sn2  36171  dihvalc  37015  mapdhval2  37508  hdmap1val2  37582  pw2f1ocnv  38106  aomclem5  38130  arearect  38302  areaquad  38303  upbdrech2  40004  lptioo2  40344  lptioo1  40345  limsupmnfuzlem  40439  limsupre3uzlem  40448  limsup10exlem  40485  coskpi2  40558  cosknegpi  40561  icccncfext  40581  cncfiooicclem1  40587  cncfiooiccre  40589  ioodvbdlimc1lem2  40628  ioodvbdlimc2lem  40630  itgioocnicc  40673  iblcncfioo  40674  volico  40680  sublevolico  40681  voliooico  40689  voliccico  40696  dirkerper  40793  dirkertrigeq  40798  dirkercncflem2  40801  fourierdlem10  40814  fourierdlem32  40836  fourierdlem33  40837  fourierdlem37  40841  fourierdlem62  40865  fourierdlem73  40876  fourierdlem74  40877  fourierdlem75  40878  fourierdlem79  40882  fourierdlem81  40884  fourierdlem82  40885  fourierdlem93  40896  fourierdlem97  40900  fourierdlem101  40904  fourierdlem103  40906  fourierdlem104  40907  sqwvfoura  40925  sqwvfourb  40926  fourierswlem  40927  fouriersw  40928  elaa2lem  40930  etransclem15  40946  etransclem19  40950  etransclem23  40954  etransclem24  40955  etransclem25  40956  ioorrnopnxrlem  41006  nnfoctbdjlem  41152  isomenndlem  41227  ovn0  41263  hsphoidmvle2  41282  hoidmv1lelem1  41288  hoidmv1lelem2  41289  hoidmv1le  41291  hoidmvlelem2  41293  hoidmvlelem3  41294  ovnhoilem1  41298  hspdifhsp  41313  hoidifhspdmvle  41317  hspmbllem1  41323  hspmbllem2  41324  hspmbl  41326  volico2  41338  ovolval4lem2  41347  ovolval5lem1  41349  afvnfundmuv  41729  ndfatafv2  41801  pfxccat3a  42005  cshword2  42013  suppmptcfin  42729  linc1  42783  ifnmfalse  43076
  Copyright terms: Public domain W3C validator