Theorem iffalse 4538

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107  {cab 2710  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  iffalsei  4539  iffalsed  4540  ifnefalse  4541  ifsb  4542  ifbi  4551  ifeq1da  4560  ifeq12da  4562  ifclda  4564  ifeqda  4565  elimif  4566  ifbothda  4567  ifid  4569  ifnot  4581  ifan  4582  ifor  4583  2if2  4584  ifcomnan  4585  elimhyp  4594  elimhyp2v  4595  elimhyp3v  4596  elimhyp4v  4597  elimdhyp  4599  keephyp2v  4601  keephyp3v  4602  dfopif  4871  opprc  4897  somin1  6135  elimdelov  7505  ovif12  7508  oevn0  8515  pw2f1olem  9076  unxpdomlem2  9251  unxpdomlem3  9252  infsupprpr  9499  oi0  9523  wemaplem2  9542  ixpiunwdom  9585  cantnfp1lem3  9675  cantnflem1  9684  dfac12lem2  10139  fin23lem14  10328  axcc2lem  10431  ttukeylem5  10508  uzin  12862  xrmax1  13154  xrmax2  13155  xrmin1  13156  xrmin2  13157  max1ALT  13165  ifle  13176  xmulneg1  13248  modifeq2int  13898  seqf1olem1  14007  seqf1olem2  14008  bcval3  14266  swrdccat  14685  pfxccat3a  14688  swrdccat3b  14690  repswswrd  14734  cshword  14741  ccatco  14786  sumrblem  15657  fsumcvg  15658  summolem2a  15661  sumss  15670  fsumcvg2  15673  sumsplit  15714  prodeq2ii  15857  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  prodss  15891  ruclem2  16175  ruclem3  16176  flodddiv4  16356  sadadd2lem2  16391  sadcp1  16396  sadcaddlem  16398  gcdn0val  16439  dfgcd2  16488  lcmn0val  16532  lcmfn0val  16560  pcgcd  16811  pcmptcl  16824  pcmpt  16825  pcmpt2  16826  pcprod  16828  fldivp1  16830  prmreclem2  16850  prmreclem4  16852  vdwlem6  16919  prmop1  16971  fvprmselelfz  16977  fvprmselgcd1  16978  ressval2  17178  xpsaddlem  17519  xpsvsca  17523  mreexexd  17592  setcepi  18038  pmtrmvd  19324  fincygsubgodd  19982  obselocv  21283  mvrf1  21545  mplcoe3  21593  mplmon2  21622  psrbagsn  21624  evlslem1  21645  mhpsclcl  21690  mhpvarcl  21691  dmatmul  21999  1mavmul  22050  mulmarep1gsum2  22076  1marepvmarrepid  22077  mdetdiag  22101  mdetrsca2  22106  mdetrlin2  22109  mdetunilem5  22118  mdetunilem7  22120  mdetunilem8  22121  mdetunilem9  22122  mndifsplit  22138  maducoeval2  22142  madugsum  22145  madurid  22146  smadiadetglem2  22174  1elcpmat  22217  decpmatid  22272  ptpjpre1  23075  ptbasfi  23085  isfcls  23513  ptcmplem2  23557  ptcmplem3  23558  dscmet  24081  dscopn  24082  icccmplem2  24339  cnmpopc  24444  iccpnfcnv  24460  xrhmeo  24462  pcoval2  24532  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  i1f1lem  25206  itg1addlem2  25214  itg1addlem3  25215  i1fres  25223  itg1climres  25232  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  itg2const2  25259  itg2seq  25260  itg2uba  25261  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  iblss  25322  iblss2  25323  itgle  25327  itgss  25329  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  bddmulibl  25356  bddiblnc  25359  ditgneg  25374  elply2  25710  coeeq2  25756  dgrle  25757  coe1termlem  25772  logcnlem3  26152  igamgam  26553  isppw  26618  isnsqf  26639  mule1  26652  sqff1o  26686  chtublem  26714  dchrelbasd  26742  bposlem1  26787  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgsneg  26824  lgsdilem  26827  lgsdir2  26833  lgsdir  26835  lgsdi  26837  lgsne0  26838  gausslemma2dlem1a  26868  2lgslem1c  26896  2lgs  26910  dchrvmasum2if  27000  ostth2lem4  27139  nosupno  27206  nosupdm  27207  nosupbday  27208  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  noinfno  27221  noinfdm  27222  noinffv  27224  maxs1  27268  maxs2  27269  mins1  27270  mins2  27271  axlowdimlem15  28214  elimifd  31775  elim2if  31776  ifeq3da  31778  ifnetrue  31779  imadifxp  31832  pmtridf1o  32253  resvval2  32443  xrge0iifcnv  32913  indval2  33012  ddeval0  33233  eulerpartlemb  33367  plymulx0  33558  signsw0glem  33564  signswmnd  33568  dfrdg2  34767  dfrdg3  34768  unisnif  34897  dfrdg4  34923  bj-xpima1sn  35837  finxpreclem2  36271  finxpreclem5  36276  matunitlindflem1  36484  poimirlem15  36503  poimirlem23  36511  mbfposadd  36535  itg2addnclem  36539  itg2addnclem3  36541  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem1  36546  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  areacirclem5  36580  areacirc  36581  heiborlem4  36682  ac6s6  37040  riotaclbgBAD  37824  cdleme27a  39238  cdleme31sn2  39260  dihvalc  40104  mapdhval2  40597  hdmap1val2  40671  metakunt6  40990  metakunt7  40991  metakunt8  40992  metakunt11  40995  metakunt12  40996  metakunt22  41006  brif1  41041  brif2  41042  brif12  41043  fsuppind  41162  dffltz  41376  pw2f1ocnv  41776  aomclem5  41800  arearect  41964  areaquad  41965  safesnsupfidom1o  42168  safesnsupfilb  42169  upbdrech2  44018  lptioo2  44347  lptioo1  44348  limsupmnfuzlem  44442  limsupre3uzlem  44451  limsup10exlem  44488  coskpi2  44582  cosknegpi  44585  icccncfext  44603  cncfiooicclem1  44609  cncfiooiccre  44611  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  itgioocnicc  44693  iblcncfioo  44694  volico  44699  sublevolico  44700  voliooico  44708  voliccico  44715  dirkerper  44812  dirkertrigeq  44817  dirkercncflem2  44820  fourierdlem10  44833  fourierdlem32  44855  fourierdlem33  44856  fourierdlem37  44860  fourierdlem62  44884  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem93  44915  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  etransclem15  44965  etransclem19  44969  etransclem23  44973  etransclem24  44974  etransclem25  44975  ioorrnopnxrlem  45022  nnfoctbdjlem  45171  isomenndlem  45246  ovn0  45282  hsphoidmvle2  45301  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1le  45310  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem1  45317  hspdifhsp  45332  hoidifhspdmvle  45336  hspmbllem1  45342  hspmbllem2  45343  hspmbl  45345  volico2  45357  ovolval4lem2  45366  ovolval5lem1  45368  afvnfundmuv  45847  ndfatafv2  45919  prproropf1olem4  46174  suppmptcfin  47055  linc1  47106  ifnmfalse  47808