Theorem iffalse 4497

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 4489	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 1062	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	eqabdv 2896	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2817	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143  {cab 2741  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  iffalsei  4498  iffalsed  4499  ifnefalse  4500  iftrueb  4501  ifsb  4502  ifbi  4511  ifeq1da  4520  ifeq12da  4522  ifclda  4524  ifeqda  4525  elimif  4526  ifbothda  4527  ifid  4529  ifnot  4541  ifan  4542  ifor  4543  2if2  4544  ifcomnan  4545  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elimdhyp  4559  keephyp2v  4561  keephyp3v  4562  dfopif  4836  opprc  4862  somin1  6135  elimdelov  7508  brif1  7509  ovif12  7512  ifmpt2v  7514  oevn0  8501  pw2f1olem  9070  unxpdomlem2  9218  unxpdomlem3  9219  infsupprpr  9467  oi0  9491  wemaplem2  9510  ixpiunwdom  9553  cantnfp1lem3  9650  cantnflem1  9659  dfac12lem2  10129  fin23lem14  10318  axcc2lem  10421  ttukeylem5  10498  indval2  12224  uzin  12899  xrmax1  13202  xrmax2  13203  xrmin1  13204  xrmin2  13205  max1ALT  13213  ifle  13224  xmulneg1  13296  modifeq2int  13971  seqf1olem1  14079  seqf1olem2  14080  bcval3  14344  swrdccat  14774  pfxccat3a  14777  swrdccat3b  14779  repswswrd  14823  cshword  14830  ccatco  14874  sumrblem  15764  fsumcvg  15765  summolem2a  15768  sumss  15777  fsumcvg2  15780  sumsplit  15821  prodeq2ii  15967  prodrblem  15985  fprodcvg  15986  prodmolem2a  15990  zprod  15993  prodss  16003  ruclem2  16289  ruclem3  16290  flodddiv4  16474  sadadd2lem2  16509  sadcp1  16514  sadcaddlem  16516  gcdn0val  16557  dfgcd2  16605  lcmn0val  16654  lcmfn0val  16682  pcgcd  16939  pcmptcl  16952  pcmpt  16953  pcmpt2  16954  pcprod  16956  fldivp1  16958  prmreclem2  16978  prmreclem4  16980  vdwlem6  17047  prmop1  17099  fvprmselelfz  17105  fvprmselgcd1  17106  ressval2  17296  xpsaddlem  17628  xpsvsca  17632  mreexexd  17705  setcepi  18146  pmtrmvd  19527  fincygsubgodd  20185  obselocv  21859  mvrf1  22116  mplcoe3  22170  mplmon2  22193  psrbagsn  22195  evlslem1  22214  mhpsclcl  22291  mhpvarcl  22292  dmatmul  22635  1mavmul  22686  mulmarep1gsum2  22712  1marepvmarrepid  22713  mdetdiag  22737  mdetrsca2  22742  mdetrlin2  22745  mdetunilem5  22754  mdetunilem7  22756  mdetunilem8  22757  mdetunilem9  22758  mndifsplit  22774  maducoeval2  22778  madugsum  22781  madurid  22782  smadiadetglem2  22810  1elcpmat  22853  decpmatid  22908  ptpjpre1  23709  ptbasfi  23719  isfcls  24147  ptcmplem2  24191  ptcmplem3  24192  dscmet  24710  dscopn  24711  icccmplem2  24962  cnmpopc  25068  iccpnfcnv  25084  xrhmeo  25086  pcoval2  25156  pcopt  25162  pcopt2  25163  pcoass  25164  pcorevlem  25166  i1f1lem  25829  itg1addlem2  25837  itg1addlem3  25838  i1fres  25845  itg1climres  25854  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  itg2const2  25881  itg2seq  25882  itg2uba  25883  itg2splitlem  25888  itg2split  25889  itg2monolem1  25890  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  iblss  25945  iblss2  25946  itgle  25950  itgss  25952  ibladdlem  25960  itgaddlem1  25963  iblabslem  25968  iblabs  25969  iblabsr  25970  iblmulc2  25971  bddmulibl  25979  bddiblnc  25982  ditgneg  25997  elply2  26334  coeeq2  26380  dgrle  26381  coe1termlem  26396  plyn0mulidp  26423  logcnlem3  26787  igamgam  27191  isppw  27256  isnsqf  27277  mule1  27290  sqff1o  27324  chtublem  27353  dchrelbasd  27381  bposlem1  27426  bposlem3  27428  bposlem5  27430  bposlem6  27431  lgsneg  27463  lgsdilem  27466  lgsdir2  27472  lgsdir  27474  lgsdi  27476  lgsne0  27477  gausslemma2dlem1a  27507  2lgslem1c  27535  2lgs  27549  dchrvmasum2if  27639  ostth2lem4  27778  nosupno  27845  nosupdm  27846  nosupbday  27847  nosupfv  27848  nosupres  27849  nosupbnd1lem1  27850  noinfno  27860  noinfdm  27861  noinffv  27863  maxs1  27911  maxs2  27912  mins1  27913  mins2  27914  abssnid  28414  abssge0  28416  axlowdimlem15  29284  elimifd  32867  elim2if  32868  ifeq3da  32870  ifnetrue  32871  imadifxp  32924  pmtridf1o  33392  resvval2  33629  xrge0iifcnv  34301  ddeval0  34603  eulerpartlemb  34736  signsw0glem  34918  signswmnd  34922  vonf1oonfo  35577  dfrdg2  36263  dfrdg3  36264  unisnif  36393  dfrdg4  36421  bj-xpima1sn  37570  finxpreclem2  38014  finxpreclem5  38019  matunitlindflem1  38245  poimirlem15  38264  poimirlem23  38272  mbfposadd  38296  itg2addnclem  38300  itg2addnclem3  38302  itg2gt0cn  38304  ibladdnclem  38305  itgaddnclem1  38307  iblabsnclem  38312  iblabsnc  38313  iblmulc2nc  38314  ftc1anclem5  38326  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  areacirclem5  38341  areacirc  38342  heiborlem4  38443  ac6s6  38799  riotaclbgBAD  39706  cdleme27a  41119  cdleme31sn2  41141  dihvalc  41985  mapdhval2  42478  hdmap1val2  42552  brif2  42973  brif12  42974  fsuppind  43302  dffltz  43346  pw2f1ocnv  43744  aomclem5  43765  arearect  43922  areaquad  43923  safesnsupfidom1o  44123  safesnsupfilb  44124  upbdrech2  46007  lptioo2  46327  lptioo1  46328  limsupmnfuzlem  46420  limsupre3uzlem  46429  limsup10exlem  46466  coskpi2  46560  cosknegpi  46563  icccncfext  46581  cncfiooicclem1  46587  cncfiooiccre  46589  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  itgioocnicc  46671  iblcncfioo  46672  volico  46677  sublevolico  46678  voliooico  46686  voliccico  46693  dirkerper  46790  dirkertrigeq  46795  dirkercncflem2  46798  fourierdlem10  46811  fourierdlem32  46833  fourierdlem33  46834  fourierdlem37  46838  fourierdlem62  46862  fourierdlem73  46873  fourierdlem74  46874  fourierdlem75  46875  fourierdlem79  46879  fourierdlem81  46881  fourierdlem82  46882  fourierdlem93  46893  fourierdlem97  46897  fourierdlem101  46901  fourierdlem103  46903  fourierdlem104  46904  sqwvfoura  46922  sqwvfourb  46923  fourierswlem  46924  fouriersw  46925  elaa2lem  46927  etransclem15  46943  etransclem19  46947  etransclem23  46951  etransclem24  46952  etransclem25  46953  ioorrnopnxrlem  47000  nnfoctbdjlem  47149  isomenndlem  47224  ovn0  47260  hsphoidmvle2  47279  hoidmv1lelem1  47285  hoidmv1lelem2  47286  hoidmv1le  47288  hoidmvlelem2  47290  hoidmvlelem3  47291  ovnhoilem1  47295  hspdifhsp  47310  hoidifhspdmvle  47314  hspmbllem1  47320  hspmbllem2  47321  hspmbl  47323  volico2  47335  ovolval4lem2  47344  ovolval5lem1  47346  afvnfundmuv  47853  ndfatafv2  47925  difmodm1lt  48079  prproropf1olem4  48232  suppmptcfin  49133  linc1  49182  discsubc  49819  oppfrcl3  49885  eloppf  49888  eloppf2  49889  ifnmfalse  50518