Theorem iffalse 4487

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 4479	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 1045	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	abbi2dv 2876	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2796	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 845   = wceq 1541   ∈ wcel 2106  {cab 2714  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4479

This theorem is referenced by:  iffalsei  4488  iffalsed  4489  ifnefalse  4490  ifsb  4491  ifbi  4500  ifeq1da  4509  ifeq12da  4511  ifclda  4513  ifeqda  4514  elimif  4515  ifbothda  4516  ifid  4518  ifnot  4530  ifan  4531  ifor  4532  2if2  4533  ifcomnan  4534  elimhyp  4543  elimhyp2v  4544  elimhyp3v  4545  elimhyp4v  4546  elimdhyp  4548  keephyp2v  4550  keephyp3v  4551  dfopif  4819  opprc  4845  somin1  6078  elimdelov  7438  ovif12  7441  oevn0  8421  pw2f1olem  8946  unxpdomlem2  9121  unxpdomlem3  9122  infsupprpr  9366  oi0  9390  wemaplem2  9409  ixpiunwdom  9452  cantnfp1lem3  9542  cantnflem1  9551  dfac12lem2  10006  fin23lem14  10195  axcc2lem  10298  ttukeylem5  10375  uzin  12724  xrmax1  13015  xrmax2  13016  xrmin1  13017  xrmin2  13018  max1ALT  13026  ifle  13037  xmulneg1  13109  modifeq2int  13759  seqf1olem1  13868  seqf1olem2  13869  bcval3  14126  swrdccat  14547  pfxccat3a  14550  swrdccat3b  14552  repswswrd  14596  cshword  14603  ccatco  14648  sumrblem  15523  fsumcvg  15524  summolem2a  15527  sumss  15536  fsumcvg2  15539  sumsplit  15580  prodeq2ii  15723  prodrblem  15739  fprodcvg  15740  prodmolem2a  15744  zprod  15747  prodss  15757  ruclem2  16041  ruclem3  16042  flodddiv4  16222  sadadd2lem2  16257  sadcp1  16262  sadcaddlem  16264  gcdn0val  16305  dfgcd2  16354  lcmn0val  16398  lcmfn0val  16426  pcgcd  16677  pcmptcl  16690  pcmpt  16691  pcmpt2  16692  pcprod  16694  fldivp1  16696  prmreclem2  16716  prmreclem4  16718  vdwlem6  16785  prmop1  16837  fvprmselelfz  16843  fvprmselgcd1  16844  ressval2  17044  xpsaddlem  17382  xpsvsca  17386  mreexexd  17455  setcepi  17901  pmtrmvd  19161  fincygsubgodd  19810  obselocv  21041  mvrf1  21300  mplcoe3  21345  mplmon2  21375  psrbagsn  21377  evlslem1  21398  mhpsclcl  21443  mhpvarcl  21444  dmatmul  21752  1mavmul  21803  mulmarep1gsum2  21829  1marepvmarrepid  21830  mdetdiag  21854  mdetrsca2  21859  mdetrlin2  21862  mdetunilem5  21871  mdetunilem7  21873  mdetunilem8  21874  mdetunilem9  21875  mndifsplit  21891  maducoeval2  21895  madugsum  21898  madurid  21899  smadiadetglem2  21927  1elcpmat  21970  decpmatid  22025  ptpjpre1  22828  ptbasfi  22838  isfcls  23266  ptcmplem2  23310  ptcmplem3  23311  dscmet  23834  dscopn  23835  icccmplem2  24092  cnmpopc  24197  iccpnfcnv  24213  xrhmeo  24215  pcoval2  24285  pcopt  24291  pcopt2  24292  pcoass  24293  pcorevlem  24295  i1f1lem  24959  itg1addlem2  24967  itg1addlem3  24968  i1fres  24976  itg1climres  24985  mbfi1fseqlem4  24989  mbfi1fseqlem5  24990  itg2const2  25012  itg2seq  25013  itg2uba  25014  itg2splitlem  25019  itg2split  25020  itg2monolem1  25021  itg2gt0  25031  itg2cnlem1  25032  itg2cnlem2  25033  iblss  25075  iblss2  25076  itgle  25080  itgss  25082  ibladdlem  25090  itgaddlem1  25093  iblabslem  25098  iblabs  25099  iblabsr  25100  iblmulc2  25101  bddmulibl  25109  bddiblnc  25112  ditgneg  25127  elply2  25463  coeeq2  25509  dgrle  25510  coe1termlem  25525  logcnlem3  25905  igamgam  26304  isppw  26369  isnsqf  26390  mule1  26403  sqff1o  26437  chtublem  26465  dchrelbasd  26493  bposlem1  26538  bposlem3  26540  bposlem5  26542  bposlem6  26543  lgsneg  26575  lgsdilem  26578  lgsdir2  26584  lgsdir  26586  lgsdi  26588  lgsne0  26589  gausslemma2dlem1a  26619  2lgslem1c  26647  2lgs  26661  dchrvmasum2if  26751  ostth2lem4  26890  nosupno  26957  nosupdm  26958  nosupbday  26959  nosupfv  26960  nosupres  26961  nosupbnd1lem1  26962  noinfno  26972  noinfdm  26973  noinffv  26975  axlowdimlem15  27613  elimifd  31171  elim2if  31172  ifeq3da  31174  imadifxp  31225  pmtridf1o  31646  resvval2  31822  xrge0iifcnv  32179  indval2  32278  ddeval0  32499  eulerpartlemb  32633  plymulx0  32824  signsw0glem  32830  signswmnd  32834  dfrdg2  34054  dfrdg3  34055  unisnif  34364  dfrdg4  34390  bj-xpima1sn  35281  finxpreclem2  35715  finxpreclem5  35720  matunitlindflem1  35927  poimirlem15  35946  poimirlem23  35954  mbfposadd  35978  itg2addnclem  35982  itg2addnclem3  35984  itg2gt0cn  35986  ibladdnclem  35987  itgaddnclem1  35989  iblabsnclem  35994  iblabsnc  35995  iblmulc2nc  35996  ftc1anclem5  36008  ftc1anclem7  36010  ftc1anclem8  36011  ftc1anc  36012  areacirclem5  36023  areacirc  36024  heiborlem4  36126  ac6s6  36484  riotaclbgBAD  37270  cdleme27a  38684  cdleme31sn2  38706  dihvalc  39550  mapdhval2  40043  hdmap1val2  40117  metakunt6  40436  metakunt7  40437  metakunt8  40438  metakunt11  40441  metakunt12  40442  metakunt22  40452  brif1  40499  brif2  40500  brif12  40501  fsuppind  40588  dffltz  40782  pw2f1ocnv  41171  aomclem5  41195  arearect  41359  areaquad  41360  safesnsupfidom1o  41396  safesnsupfilb  41397  upbdrech2  43232  lptioo2  43558  lptioo1  43559  limsupmnfuzlem  43653  limsupre3uzlem  43662  limsup10exlem  43699  coskpi2  43793  cosknegpi  43796  icccncfext  43814  cncfiooicclem1  43820  cncfiooiccre  43822  ioodvbdlimc1lem2  43859  ioodvbdlimc2lem  43861  itgioocnicc  43904  iblcncfioo  43905  volico  43910  sublevolico  43911  voliooico  43919  voliccico  43926  dirkerper  44023  dirkertrigeq  44028  dirkercncflem2  44031  fourierdlem10  44044  fourierdlem32  44066  fourierdlem33  44067  fourierdlem37  44071  fourierdlem62  44095  fourierdlem73  44106  fourierdlem74  44107  fourierdlem75  44108  fourierdlem79  44112  fourierdlem81  44114  fourierdlem82  44115  fourierdlem93  44126  fourierdlem97  44130  fourierdlem101  44134  fourierdlem103  44136  fourierdlem104  44137  sqwvfoura  44155  sqwvfourb  44156  fourierswlem  44157  fouriersw  44158  elaa2lem  44160  etransclem15  44176  etransclem19  44180  etransclem23  44184  etransclem24  44185  etransclem25  44186  ioorrnopnxrlem  44233  nnfoctbdjlem  44380  isomenndlem  44455  ovn0  44491  hsphoidmvle2  44510  hoidmv1lelem1  44516  hoidmv1lelem2  44517  hoidmv1le  44519  hoidmvlelem2  44521  hoidmvlelem3  44522  ovnhoilem1  44526  hspdifhsp  44541  hoidifhspdmvle  44545  hspmbllem1  44551  hspmbllem2  44552  hspmbl  44554  volico2  44566  ovolval4lem2  44575  ovolval5lem1  44577  afvnfundmuv  45047  ndfatafv2  45119  prproropf1olem4  45374  suppmptcfin  46131  linc1  46182  ifnmfalse  46881