Theorem iffalse 4501

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.

Step	Hyp	Ref	Expression
1		df-if 4493	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 1062	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	eqabdv 2899	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2820	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146  {cab 2744  ifcif 4492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-if 4493

This theorem is used by:  iffalsei  4502  iffalsed  4503  ifnefalse  4504  iftrueb  4505  ifsb  4506  ifbi  4515  ifeq1da  4524  ifeq12da  4526  ifclda  4528  ifeqda  4529  elimif  4530  ifbothda  4531  ifid  4533  ifnot  4545  ifan  4546  ifor  4547  2if2  4548  ifcomnan  4549  elimhyp  4558  elimhyp2v  4559  elimhyp3v  4560  elimhyp4v  4561  elimdhyp  4563  keephyp2v  4565  keephyp3v  4566  dfopif  4840  opprc  4866  somin1  6138  elimdelov  7519  brif1  7520  ovif12  7523  ifmpt2v  7525  oevn0  8509  pw2f1olem  9079  unxpdomlem2  9227  unxpdomlem3  9228  infsupprpr  9476  oi0  9500  wemaplem2  9519  ixpiunwdom  9562  cantnfp1lem3  9659  cantnflem1  9668  dfac12lem2  10147  fin23lem14  10335  axcc2lem  10438  ttukeylem5  10515  indval2  12241  uzin  12916  xrmax1  13219  xrmax2  13220  xrmin1  13221  xrmin2  13222  max1ALT  13230  ifle  13241  xmulneg1  13313  modifeq2int  13989  seqf1olem1  14097  seqf1olem2  14098  bcval3  14362  swrdccat  14796  pfxccat3a  14799  swrdccat3b  14801  repswswrd  14847  cshword  14854  ccatco  14898  sumrblem  15788  fsumcvg  15789  summolem2a  15792  sumss  15801  fsumcvg2  15804  sumsplit  15845  prodeq2ii  15991  prodrblem  16009  fprodcvg  16010  prodmolem2a  16014  zprod  16017  prodss  16027  ruclem2  16313  ruclem3  16314  flodddiv4  16498  sadadd2lem2  16533  sadcp1  16538  sadcaddlem  16540  gcdn0val  16581  dfgcd2  16629  lcmn0val  16678  lcmfn0val  16706  pcgcd  16963  pcmptcl  16976  pcmpt  16977  pcmpt2  16978  pcprod  16980  fldivp1  16982  prmreclem2  17002  prmreclem4  17004  vdwlem6  17071  prmop1  17123  fvprmselelfz  17129  fvprmselgcd1  17130  ressval2  17320  xpsaddlem  17652  xpsvsca  17656  mreexexd  17729  setcepi  18170  pmtrmvd  19557  fincygsubgodd  20215  obselocv  21915  mvrf1  22172  mplcoe3  22226  mplmon2  22249  psrbagsn  22251  evlslem1  22270  mhpsclcl  22347  mhpvarcl  22348  dmatmul  22691  1mavmul  22742  mulmarep1gsum2  22768  1marepvmarrepid  22769  mdetdiag  22793  mdetrsca2  22798  mdetrlin2  22801  mdetunilem5  22810  mdetunilem7  22812  mdetunilem8  22813  mdetunilem9  22814  mndifsplit  22830  maducoeval2  22834  madugsum  22837  madurid  22838  smadiadetglem2  22866  1elcpmat  22909  decpmatid  22964  ptpjpre1  23765  ptbasfi  23775  isfcls  24203  ptcmplem2  24247  ptcmplem3  24248  dscmet  24766  dscopn  24767  icccmplem2  25018  cnmpopc  25124  iccpnfcnv  25140  xrhmeo  25142  pcoval2  25212  pcopt  25218  pcopt2  25219  pcoass  25220  pcorevlem  25222  i1f1lem  25885  itg1addlem2  25893  itg1addlem3  25894  i1fres  25901  itg1climres  25910  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  itg2const2  25937  itg2seq  25938  itg2uba  25939  itg2splitlem  25944  itg2split  25945  itg2monolem1  25946  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  iblss  26001  iblss2  26002  itgle  26006  itgss  26008  ibladdlem  26016  itgaddlem1  26019  iblabslem  26024  iblabs  26025  iblabsr  26026  iblmulc2  26027  bddmulibl  26035  bddiblnc  26038  ditgneg  26053  elply2  26390  coeeq2  26436  dgrle  26437  coe1termlem  26452  plyn0mulidp  26479  logcnlem3  26846  igamgam  27250  isppw  27315  isnsqf  27336  mule1  27349  sqff1o  27383  chtublem  27412  dchrelbasd  27440  bposlem1  27485  bposlem3  27487  bposlem5  27489  bposlem6  27490  lgsneg  27522  lgsdilem  27525  lgsdir2  27531  lgsdir  27533  lgsdi  27535  lgsne0  27536  gausslemma2dlem1a  27566  2lgslem1c  27594  2lgs  27608  dchrvmasum2if  27698  ostth2lem4  27837  nosupno  27904  nosupdm  27905  nosupbday  27906  nosupfv  27907  nosupres  27908  nosupbnd1lem1  27909  noinfno  27919  noinfdm  27920  noinffv  27922  maxs1  27970  maxs2  27971  mins1  27972  mins2  27973  abssnid  28473  abssge0  28475  axlowdimlem15  29343  elimifd  32926  elim2if  32927  ifeq3da  32929  ifnetrue  32930  imadifxp  32983  pmtridf1o  33445  resvval2  33682  xrge0iifcnv  34354  ddeval0  34656  eulerpartlemb  34789  signsw0glem  34971  signswmnd  34975  vonf1oonfo  35622  dfrdg2  36305  dfrdg3  36306  unisnif  36435  dfrdg4  36463  bj-xpima1sn  37632  finxpreclem2  38076  finxpreclem5  38081  matunitlindflem1  38307  poimirlem15  38326  poimirlem23  38334  mbfposadd  38358  itg2addnclem  38362  itg2addnclem3  38364  itg2gt0cn  38366  ibladdnclem  38367  itgaddnclem1  38369  iblabsnclem  38374  iblabsnc  38375  iblmulc2nc  38376  ftc1anclem5  38388  ftc1anclem7  38390  ftc1anclem8  38391  ftc1anc  38392  areacirclem5  38403  areacirc  38404  heiborlem4  38505  ac6s6  38861  riotaclbgBAD  39768  cdleme27a  41181  cdleme31sn2  41203  dihvalc  42047  mapdhval2  42540  hdmap1val2  42614  brif2  43035  brif12  43036  fsuppind  43362  dffltz  43406  pw2f1ocnv  43804  aomclem5  43825  arearect  43982  areaquad  43983  safesnsupfidom1o  44183  safesnsupfilb  44184  upbdrech2  46067  lptioo2  46387  lptioo1  46388  limsupmnfuzlem  46480  limsupre3uzlem  46489  limsup10exlem  46526  coskpi2  46620  cosknegpi  46623  icccncfext  46641  cncfiooicclem1  46647  cncfiooiccre  46649  ioodvbdlimc1lem2  46686  ioodvbdlimc2lem  46688  itgioocnicc  46731  iblcncfioo  46732  volico  46737  sublevolico  46738  voliooico  46746  voliccico  46753  dirkerper  46850  dirkertrigeq  46855  dirkercncflem2  46858  fourierdlem10  46871  fourierdlem32  46893  fourierdlem33  46894  fourierdlem37  46898  fourierdlem62  46922  fourierdlem73  46933  fourierdlem74  46934  fourierdlem75  46935  fourierdlem79  46939  fourierdlem81  46941  fourierdlem82  46942  fourierdlem93  46953  fourierdlem97  46957  fourierdlem101  46961  fourierdlem103  46963  fourierdlem104  46964  sqwvfoura  46982  sqwvfourb  46983  fourierswlem  46984  fouriersw  46985  elaa2lem  46987  etransclem15  47003  etransclem19  47007  etransclem23  47011  etransclem24  47012  etransclem25  47013  ioorrnopnxrlem  47060  nnfoctbdjlem  47209  isomenndlem  47284  ovn0  47320  hsphoidmvle2  47339  hoidmv1lelem1  47345  hoidmv1lelem2  47346  hoidmv1le  47348  hoidmvlelem2  47350  hoidmvlelem3  47351  ovnhoilem1  47355  hspdifhsp  47370  hoidifhspdmvle  47374  hspmbllem1  47380  hspmbllem2  47381  hspmbl  47383  volico2  47395  ovolval4lem2  47404  ovolval5lem1  47406  afvnfundmuv  47916  ndfatafv2  47988  difmodm1lt  48142  prproropf1olem4  48295  suppmptcfin  49196  linc1  49245  discsubc  49882  oppfrcl3  49948  eloppf  49951  eloppf2  49952  ifnmfalse  50581