Theorem iffalse 4496

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143  {cab 2741  ifcif 4487

This proof depends on 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 proof 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 4488

This theorem is used by:  iffalsei  4497  iffalsed  4498  ifnefalse  4499  iftrueb  4500  ifsb  4501  ifbi  4510  ifeq1da  4519  ifeq12da  4521  ifclda  4523  ifeqda  4524  elimif  4525  ifbothda  4526  ifid  4528  ifnot  4540  ifan  4541  ifor  4542  2if2  4543  ifcomnan  4544  elimhyp  4553  elimhyp2v  4554  elimhyp3v  4555  elimhyp4v  4556  elimdhyp  4558  keephyp2v  4560  keephyp3v  4561  dfopif  4835  opprc  4861  somin1  6133  elimdelov  7506  brif1  7507  ovif12  7510  ifmpt2v  7512  oevn0  8496  pw2f1olem  9065  unxpdomlem2  9213  unxpdomlem3  9214  infsupprpr  9462  oi0  9486  wemaplem2  9505  ixpiunwdom  9548  cantnfp1lem3  9645  cantnflem1  9654  dfac12lem2  10133  fin23lem14  10321  axcc2lem  10424  ttukeylem5  10501  indval2  12227  uzin  12902  xrmax1  13205  xrmax2  13206  xrmin1  13207  xrmin2  13208  max1ALT  13216  ifle  13227  xmulneg1  13299  modifeq2int  13974  seqf1olem1  14082  seqf1olem2  14083  bcval3  14347  swrdccat  14777  pfxccat3a  14780  swrdccat3b  14782  repswswrd  14826  cshword  14833  ccatco  14877  sumrblem  15767  fsumcvg  15768  summolem2a  15771  sumss  15780  fsumcvg2  15783  sumsplit  15824  prodeq2ii  15970  prodrblem  15988  fprodcvg  15989  prodmolem2a  15993  zprod  15996  prodss  16006  ruclem2  16292  ruclem3  16293  flodddiv4  16477  sadadd2lem2  16512  sadcp1  16517  sadcaddlem  16519  gcdn0val  16560  dfgcd2  16608  lcmn0val  16657  lcmfn0val  16685  pcgcd  16942  pcmptcl  16955  pcmpt  16956  pcmpt2  16957  pcprod  16959  fldivp1  16961  prmreclem2  16981  prmreclem4  16983  vdwlem6  17050  prmop1  17102  fvprmselelfz  17108  fvprmselgcd1  17109  ressval2  17299  xpsaddlem  17631  xpsvsca  17635  mreexexd  17708  setcepi  18149  pmtrmvd  19530  fincygsubgodd  20188  obselocv  21887  mvrf1  22144  mplcoe3  22198  mplmon2  22221  psrbagsn  22223  evlslem1  22242  mhpsclcl  22319  mhpvarcl  22320  dmatmul  22663  1mavmul  22714  mulmarep1gsum2  22740  1marepvmarrepid  22741  mdetdiag  22765  mdetrsca2  22770  mdetrlin2  22773  mdetunilem5  22782  mdetunilem7  22784  mdetunilem8  22785  mdetunilem9  22786  mndifsplit  22802  maducoeval2  22806  madugsum  22809  madurid  22810  smadiadetglem2  22838  1elcpmat  22881  decpmatid  22936  ptpjpre1  23737  ptbasfi  23747  isfcls  24175  ptcmplem2  24219  ptcmplem3  24220  dscmet  24738  dscopn  24739  icccmplem2  24990  cnmpopc  25096  iccpnfcnv  25112  xrhmeo  25114  pcoval2  25184  pcopt  25190  pcopt2  25191  pcoass  25192  pcorevlem  25194  i1f1lem  25857  itg1addlem2  25865  itg1addlem3  25866  i1fres  25873  itg1climres  25882  mbfi1fseqlem4  25886  mbfi1fseqlem5  25887  itg2const2  25909  itg2seq  25910  itg2uba  25911  itg2splitlem  25916  itg2split  25917  itg2monolem1  25918  itg2gt0  25928  itg2cnlem1  25929  itg2cnlem2  25930  iblss  25973  iblss2  25974  itgle  25978  itgss  25980  ibladdlem  25988  itgaddlem1  25991  iblabslem  25996  iblabs  25997  iblabsr  25998  iblmulc2  25999  bddmulibl  26007  bddiblnc  26010  ditgneg  26025  elply2  26362  coeeq2  26408  dgrle  26409  coe1termlem  26424  plyn0mulidp  26451  logcnlem3  26818  igamgam  27222  isppw  27287  isnsqf  27308  mule1  27321  sqff1o  27355  chtublem  27384  dchrelbasd  27412  bposlem1  27457  bposlem3  27459  bposlem5  27461  bposlem6  27462  lgsneg  27494  lgsdilem  27497  lgsdir2  27503  lgsdir  27505  lgsdi  27507  lgsne0  27508  gausslemma2dlem1a  27538  2lgslem1c  27566  2lgs  27580  dchrvmasum2if  27670  ostth2lem4  27809  nosupno  27876  nosupdm  27877  nosupbday  27878  nosupfv  27879  nosupres  27880  nosupbnd1lem1  27881  noinfno  27891  noinfdm  27892  noinffv  27894  maxs1  27942  maxs2  27943  mins1  27944  mins2  27945  abssnid  28445  abssge0  28447  axlowdimlem15  29315  elimifd  32898  elim2if  32899  ifeq3da  32901  ifnetrue  32902  imadifxp  32955  pmtridf1o  33423  resvval2  33660  xrge0iifcnv  34332  ddeval0  34634  eulerpartlemb  34767  signsw0glem  34949  signswmnd  34953  vonf1oonfo  35607  dfrdg2  36293  dfrdg3  36294  unisnif  36423  dfrdg4  36451  bj-xpima1sn  37620  finxpreclem2  38064  finxpreclem5  38069  matunitlindflem1  38295  poimirlem15  38314  poimirlem23  38322  mbfposadd  38346  itg2addnclem  38350  itg2addnclem3  38352  itg2gt0cn  38354  ibladdnclem  38355  itgaddnclem1  38357  iblabsnclem  38362  iblabsnc  38363  iblmulc2nc  38364  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  areacirclem5  38391  areacirc  38392  heiborlem4  38493  ac6s6  38849  riotaclbgBAD  39756  cdleme27a  41169  cdleme31sn2  41191  dihvalc  42035  mapdhval2  42528  hdmap1val2  42602  brif2  43023  brif12  43024  fsuppind  43350  dffltz  43394  pw2f1ocnv  43792  aomclem5  43813  arearect  43970  areaquad  43971  safesnsupfidom1o  44171  safesnsupfilb  44172  upbdrech2  46055  lptioo2  46375  lptioo1  46376  limsupmnfuzlem  46468  limsupre3uzlem  46477  limsup10exlem  46514  coskpi2  46608  cosknegpi  46611  icccncfext  46629  cncfiooicclem1  46635  cncfiooiccre  46637  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  itgioocnicc  46719  iblcncfioo  46720  volico  46725  sublevolico  46726  voliooico  46734  voliccico  46741  dirkerper  46838  dirkertrigeq  46843  dirkercncflem2  46846  fourierdlem10  46859  fourierdlem32  46881  fourierdlem33  46882  fourierdlem37  46886  fourierdlem62  46910  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem79  46927  fourierdlem81  46929  fourierdlem82  46930  fourierdlem93  46941  fourierdlem97  46945  fourierdlem101  46949  fourierdlem103  46951  fourierdlem104  46952  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  elaa2lem  46975  etransclem15  46991  etransclem19  46995  etransclem23  46999  etransclem24  47000  etransclem25  47001  ioorrnopnxrlem  47048  nnfoctbdjlem  47197  isomenndlem  47272  ovn0  47308  hsphoidmvle2  47327  hoidmv1lelem1  47333  hoidmv1lelem2  47334  hoidmv1le  47336  hoidmvlelem2  47338  hoidmvlelem3  47339  ovnhoilem1  47343  hspdifhsp  47358  hoidifhspdmvle  47362  hspmbllem1  47368  hspmbllem2  47369  hspmbl  47371  volico2  47383  ovolval4lem2  47392  ovolval5lem1  47394  afvnfundmuv  47904  ndfatafv2  47976  difmodm1lt  48130  prproropf1olem4  48283  suppmptcfin  49184  linc1  49233  discsubc  49870  oppfrcl3  49936  eloppf  49939  eloppf2  49940  ifnmfalse  50569