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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147  {cab 2741  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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  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  4840  opprc  4857  somin1  6139  elimdelov  7539  brif1  7540  ovif12  7543  ifmpt2v  7545  oevn0  8551  pw2f1olem  9128  unxpdomlem2  9276  unxpdomlem3  9277  infsupprpr  9525  oi0  9549  wemaplem2  9568  ixpiunwdom  9611  cantnfp1lem3  9708  cantnflem1  9717  dfac12lem2  10250  fin23lem14  10438  axcc2lem  10541  ttukeylem5  10618  indval2  12352  uzin  13028  xrmax1  13332  xrmax2  13333  xrmin1  13334  xrmin2  13335  max1ALT  13343  ifle  13354  xmulneg1  13426  modifeq2int  14103  seqf1olem1  14211  seqf1olem2  14212  bcval3  14477  swrdccat  14912  pfxccat3a  14915  swrdccat3b  14917  repswswrd  14963  cshword  14970  ccatco  15014  sumrblem  15906  fsumcvg  15907  summolem2a  15910  sumss  15919  fsumcvg2  15922  sumsplit  15963  prodeq2ii  16109  prodrblem  16125  fprodcvg  16126  prodmolem2a  16130  zprod  16133  prodss  16143  ruclem2  16429  ruclem3  16430  flodddiv4  16614  sadadd2lem2  16649  sadcp1  16654  sadcaddlem  16656  gcdn0val  16697  dfgcd2  16748  lcmn0val  16799  lcmfn0val  16827  pcgcd  17085  pcmptcl  17098  pcmpt  17099  pcmpt2  17100  pcprod  17102  fldivp1  17104  prmreclem2  17124  prmreclem4  17126  vdwlem6  17193  prmop1  17245  fvprmselelfz  17251  fvprmselgcd1  17252  ressval2  17442  xpsaddlem  17774  xpsvsca  17778  mreexexd  17851  setcepi  18292  pmtrmvd  19700  fincygsubgodd  20358  obselocv  22064  mvrf1  22323  mplcoe3  22377  mplmon2  22400  psrbagsn  22402  evlslem1  22421  mhpsclcl  22498  mhpvarcl  22499  dmatmul  22842  1mavmul  22893  mulmarep1gsum2  22919  1marepvmarrepid  22920  mdetdiag  22944  mdetrsca2  22949  mdetrlin2  22952  mdetunilem5  22961  mdetunilem7  22963  mdetunilem8  22964  mdetunilem9  22965  mndifsplit  22981  maducoeval2  22985  madugsum  22988  madurid  22989  smadiadetglem2  23017  matunitlindflem1  23024  1elcpmat  23063  decpmatid  23118  ptpjpre1  23920  ptbasfi  23930  isfcls  24358  ptcmplem2  24402  ptcmplem3  24403  dscmet  24921  dscopn  24922  icccmplem2  25173  cnmpopc  25279  iccpnfcnv  25295  xrhmeo  25297  pcoval2  25367  pcopt  25373  pcopt2  25374  pcoass  25375  pcorevlem  25377  i1f1lem  26040  itg1addlem2  26048  itg1addlem3  26049  i1fres  26056  itg1climres  26065  mbfi1fseqlem4  26069  mbfi1fseqlem5  26070  itg2const2  26092  itg2seq  26093  itg2uba  26094  itg2splitlem  26099  itg2split  26100  itg2monolem1  26101  itg2gt0  26111  itg2cnlem1  26112  itg2cnlem2  26113  iblss  26155  iblss2  26156  itgle  26160  itgss  26162  ibladdlem  26170  itgaddlem1  26173  iblabslem  26178  iblabs  26179  iblabsr  26180  iblmulc2  26181  bddmulibl  26189  bddiblnc  26192  ditgneg  26207  elply2  26544  coeeq2  26591  dgrle  26592  coe1termlem  26607  plyn0mulidp  26632  logcnlem3  27002  igamgam  27406  isppw  27471  isnsqf  27492  mule1  27505  sqff1o  27539  chtublem  27568  dchrelbasd  27596  bposlem1  27641  bposlem3  27643  bposlem5  27645  bposlem6  27646  lgsneg  27678  lgsdilem  27681  lgsdir2  27687  lgsdir  27689  lgsdi  27691  lgsne0  27692  gausslemma2dlem1a  27722  2lgslem1c  27750  2lgs  27764  dchrvmasum2if  27854  ostth2lem4  27993  nosupno  28090  nosupdm  28091  nosupbday  28092  nosupfv  28093  nosupres  28094  nosupbnd1lem1  28095  noinfno  28105  noinfdm  28106  noinffv  28108  maxs1  28156  maxs2  28157  mins1  28158  mins2  28159  abssnid  28659  abssge0  28661  axlowdimlem15  29564  elimifd  33211  elim2if  33212  ifeq3da  33214  ifnetrue  33215  imadifxp  33267  pmtridf1o  33725  resvval2  33962  xrge0iifcnv  34635  ddeval0  34938  eulerpartlemb  35070  signsw0glem  35252  signswmnd  35256  jaeqifi  35782  ordunmax  35792  soinfdom  35800  vonf1oonfo  36049  onf1oracwevd  36052  onprcf1of1ord  36055  dfrdg2  36735  dfrdg3  36736  unisnif  36865  dfrdg4  36893  bj-xpima1sn  38047  finxpreclem2  38505  finxpreclem5  38510  poimirlem15  38745  poimirlem23  38753  mbfposadd  38777  itg2addnclem  38781  itg2addnclem3  38783  itg2gt0cn  38785  ibladdnclem  38786  itgaddnclem1  38788  iblabsnclem  38793  iblabsnc  38794  iblmulc2nc  38795  ftc1anclem5  38807  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  areacirclem5  38822  areacirc  38823  heiborlem4  38940  ac6s6  39296  riotaclbgBAD  40203  cdleme27a  41616  cdleme31sn2  41638  dihvalc  42482  mapdhval2  42975  hdmap1val2  43049  brif2  43471  brif12  43472  fsuppind  43811  dffltz  43863  pw2f1ocnv  44237  aomclem5  44253  arearect  44409  areaquad  44410  safesnsupfidom1o  44610  safesnsupfilb  44611  upbdrech2  46529  lptioo2  46848  lptioo1  46849  limsupmnfuzlem  46941  limsupre3uzlem  46950  limsup10exlem  46987  coskpi2  47081  cosknegpi  47084  icccncfext  47102  cncfiooicclem1  47108  cncfiooiccre  47110  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  itgioocnicc  47192  iblcncfioo  47193  volico  47198  sublevolico  47199  voliooico  47207  voliccico  47214  dirkerper  47311  dirkertrigeq  47316  dirkercncflem2  47319  fourierdlem10  47332  fourierdlem32  47354  fourierdlem33  47355  fourierdlem37  47359  fourierdlem62  47383  fourierdlem73  47394  fourierdlem74  47395  fourierdlem75  47396  fourierdlem79  47400  fourierdlem81  47402  fourierdlem82  47403  fourierdlem93  47414  fourierdlem97  47418  fourierdlem101  47422  fourierdlem103  47424  fourierdlem104  47425  sqwvfoura  47443  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  elaa2lem  47448  etransclem15  47464  etransclem19  47468  etransclem23  47472  etransclem24  47473  etransclem25  47474  ioorrnopnxrlem  47521  nnfoctbdjlem  47670  isomenndlem  47745  ovn0  47781  hsphoidmvle2  47800  hoidmv1lelem1  47806  hoidmv1lelem2  47807  hoidmv1le  47809  hoidmvlelem2  47811  hoidmvlelem3  47812  ovnhoilem1  47816  hspdifhsp  47831  hoidifhspdmvle  47835  hspmbllem1  47841  hspmbllem2  47842  hspmbl  47844  volico2  47856  ovolval4lem2  47865  ovolval5lem1  47867  aiotaexim  48373  afvnfundmuv  48414  ndfatafv2  48486  difmodm1lt  48640  prproropf1olem4  48793  suppmptcfin  49693  linc1  49742  discsubc  50383  oppfrcl3  50451  eloppf  50454  eloppf2  50455  ifnmfalse  51139