Theorem iffalse 4494

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

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

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  iffalsei  4495  iffalsed  4496  ifnefalse  4497  iftrueb  4498  ifsb  4499  ifbi  4508  ifeq1da  4517  ifeq12da  4519  ifclda  4521  ifeqda  4522  elimif  4523  ifbothda  4524  ifid  4526  ifnot  4538  ifan  4539  ifor  4540  2if2  4541  ifcomnan  4542  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elimdhyp  4556  keephyp2v  4558  keephyp3v  4559  dfopif  4833  opprc  4859  somin1  6131  elimdelov  7513  brif1  7514  ovif12  7517  ifmpt2v  7519  oevn0  8506  pw2f1olem  9083  unxpdomlem2  9231  unxpdomlem3  9232  infsupprpr  9480  oi0  9504  wemaplem2  9523  ixpiunwdom  9566  cantnfp1lem3  9663  cantnflem1  9672  dfac12lem2  10151  fin23lem14  10339  axcc2lem  10442  ttukeylem5  10519  indval2  12251  uzin  12927  xrmax1  13231  xrmax2  13232  xrmin1  13233  xrmin2  13234  max1ALT  13242  ifle  13253  xmulneg1  13325  modifeq2int  14001  seqf1olem1  14109  seqf1olem2  14110  bcval3  14374  swrdccat  14808  pfxccat3a  14811  swrdccat3b  14813  repswswrd  14859  cshword  14866  ccatco  14910  sumrblem  15801  fsumcvg  15802  summolem2a  15805  sumss  15814  fsumcvg2  15817  sumsplit  15858  prodeq2ii  16004  prodrblem  16022  fprodcvg  16023  prodmolem2a  16027  zprod  16030  prodss  16040  ruclem2  16326  ruclem3  16327  flodddiv4  16511  sadadd2lem2  16546  sadcp1  16551  sadcaddlem  16553  gcdn0val  16594  dfgcd2  16642  lcmn0val  16691  lcmfn0val  16719  pcgcd  16976  pcmptcl  16989  pcmpt  16990  pcmpt2  16991  pcprod  16993  fldivp1  16995  prmreclem2  17015  prmreclem4  17017  vdwlem6  17084  prmop1  17136  fvprmselelfz  17142  fvprmselgcd1  17143  ressval2  17333  xpsaddlem  17665  xpsvsca  17669  mreexexd  17742  setcepi  18183  pmtrmvd  19589  fincygsubgodd  20247  obselocv  21947  mvrf1  22206  mplcoe3  22260  mplmon2  22283  psrbagsn  22285  evlslem1  22304  mhpsclcl  22381  mhpvarcl  22382  dmatmul  22725  1mavmul  22776  mulmarep1gsum2  22802  1marepvmarrepid  22803  mdetdiag  22827  mdetrsca2  22832  mdetrlin2  22835  mdetunilem5  22844  mdetunilem7  22846  mdetunilem8  22847  mdetunilem9  22848  mndifsplit  22864  maducoeval2  22868  madugsum  22871  madurid  22872  smadiadetglem2  22900  matunitlindflem1  22907  1elcpmat  22946  decpmatid  23001  ptpjpre1  23803  ptbasfi  23813  isfcls  24241  ptcmplem2  24285  ptcmplem3  24286  dscmet  24804  dscopn  24805  icccmplem2  25056  cnmpopc  25162  iccpnfcnv  25178  xrhmeo  25180  pcoval2  25250  pcopt  25256  pcopt2  25257  pcoass  25258  pcorevlem  25260  i1f1lem  25923  itg1addlem2  25931  itg1addlem3  25932  i1fres  25939  itg1climres  25948  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  itg2const2  25975  itg2seq  25976  itg2uba  25977  itg2splitlem  25982  itg2split  25983  itg2monolem1  25984  itg2gt0  25994  itg2cnlem1  25995  itg2cnlem2  25996  iblss  26039  iblss2  26040  itgle  26044  itgss  26046  ibladdlem  26054  itgaddlem1  26057  iblabslem  26062  iblabs  26063  iblabsr  26064  iblmulc2  26065  bddmulibl  26073  bddiblnc  26076  ditgneg  26091  elply2  26428  coeeq2  26475  dgrle  26476  coe1termlem  26491  plyn0mulidp  26518  logcnlem3  26889  igamgam  27293  isppw  27358  isnsqf  27379  mule1  27392  sqff1o  27426  chtublem  27455  dchrelbasd  27483  bposlem1  27528  bposlem3  27530  bposlem5  27532  bposlem6  27533  lgsneg  27565  lgsdilem  27568  lgsdir2  27574  lgsdir  27576  lgsdi  27578  lgsne0  27579  gausslemma2dlem1a  27609  2lgslem1c  27637  2lgs  27651  dchrvmasum2if  27741  ostth2lem4  27880  nosupno  27947  nosupdm  27948  nosupbday  27949  nosupfv  27950  nosupres  27951  nosupbnd1lem1  27952  noinfno  27962  noinfdm  27963  noinffv  27965  maxs1  28013  maxs2  28014  mins1  28015  mins2  28016  abssnid  28516  abssge0  28518  axlowdimlem15  29421  elimifd  33026  elim2if  33027  ifeq3da  33029  ifnetrue  33030  imadifxp  33082  pmtridf1o  33542  resvval2  33779  xrge0iifcnv  34451  ddeval0  34754  eulerpartlemb  34887  signsw0glem  35069  signswmnd  35073  vonf1oonfo  35720  dfrdg2  36380  dfrdg3  36381  unisnif  36510  dfrdg4  36538  bj-xpima1sn  37708  finxpreclem2  38152  finxpreclem5  38157  poimirlem15  38392  poimirlem23  38400  mbfposadd  38424  itg2addnclem  38428  itg2addnclem3  38430  itg2gt0cn  38432  ibladdnclem  38433  itgaddnclem1  38435  iblabsnclem  38440  iblabsnc  38441  iblmulc2nc  38442  ftc1anclem5  38454  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  areacirclem5  38469  areacirc  38470  heiborlem4  38572  ac6s6  38928  riotaclbgBAD  39835  cdleme27a  41248  cdleme31sn2  41270  dihvalc  42114  mapdhval2  42607  hdmap1val2  42681  brif2  43102  brif12  43103  fsuppind  43444  dffltz  43488  pw2f1ocnv  43886  aomclem5  43907  arearect  44064  areaquad  44065  safesnsupfidom1o  44265  safesnsupfilb  44266  upbdrech2  46149  lptioo2  46469  lptioo1  46470  limsupmnfuzlem  46562  limsupre3uzlem  46571  limsup10exlem  46608  coskpi2  46702  cosknegpi  46705  icccncfext  46723  cncfiooicclem1  46729  cncfiooiccre  46731  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  itgioocnicc  46813  iblcncfioo  46814  volico  46819  sublevolico  46820  voliooico  46828  voliccico  46835  dirkerper  46932  dirkertrigeq  46937  dirkercncflem2  46940  fourierdlem10  46953  fourierdlem32  46975  fourierdlem33  46976  fourierdlem37  46980  fourierdlem62  47004  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem79  47021  fourierdlem81  47023  fourierdlem82  47024  fourierdlem93  47035  fourierdlem97  47039  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  elaa2lem  47069  etransclem15  47085  etransclem19  47089  etransclem23  47093  etransclem24  47094  etransclem25  47095  ioorrnopnxrlem  47142  nnfoctbdjlem  47291  isomenndlem  47366  ovn0  47402  hsphoidmvle2  47421  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmv1le  47430  hoidmvlelem2  47432  hoidmvlelem3  47433  ovnhoilem1  47437  hspdifhsp  47452  hoidifhspdmvle  47456  hspmbllem1  47462  hspmbllem2  47463  hspmbl  47465  volico2  47477  ovolval4lem2  47486  ovolval5lem1  47488  afvnfundmuv  48035  ndfatafv2  48107  difmodm1lt  48261  prproropf1olem4  48414  suppmptcfin  49314  linc1  49363  discsubc  49998  oppfrcl3  50064  eloppf  50067  eloppf2  50068  ifnmfalse  50700