Theorem iffalse 4537

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106  {cab 2709  ifcif 4528

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  iffalsei  4538  iffalsed  4539  ifnefalse  4540  ifsb  4541  ifbi  4550  ifeq1da  4559  ifeq12da  4561  ifclda  4563  ifeqda  4564  elimif  4565  ifbothda  4566  ifid  4568  ifnot  4580  ifan  4581  ifor  4582  2if2  4583  ifcomnan  4584  elimhyp  4593  elimhyp2v  4594  elimhyp3v  4595  elimhyp4v  4596  elimdhyp  4598  keephyp2v  4600  keephyp3v  4601  dfopif  4870  opprc  4896  somin1  6134  elimdelov  7507  ovif12  7510  oevn0  8517  pw2f1olem  9078  unxpdomlem2  9253  unxpdomlem3  9254  infsupprpr  9501  oi0  9525  wemaplem2  9544  ixpiunwdom  9587  cantnfp1lem3  9677  cantnflem1  9686  dfac12lem2  10141  fin23lem14  10330  axcc2lem  10433  ttukeylem5  10510  uzin  12864  xrmax1  13156  xrmax2  13157  xrmin1  13158  xrmin2  13159  max1ALT  13167  ifle  13178  xmulneg1  13250  modifeq2int  13900  seqf1olem1  14009  seqf1olem2  14010  bcval3  14268  swrdccat  14687  pfxccat3a  14690  swrdccat3b  14692  repswswrd  14736  cshword  14743  ccatco  14788  sumrblem  15659  fsumcvg  15660  summolem2a  15663  sumss  15672  fsumcvg2  15675  sumsplit  15716  prodeq2ii  15859  prodrblem  15875  fprodcvg  15876  prodmolem2a  15880  zprod  15883  prodss  15893  ruclem2  16177  ruclem3  16178  flodddiv4  16358  sadadd2lem2  16393  sadcp1  16398  sadcaddlem  16400  gcdn0val  16441  dfgcd2  16490  lcmn0val  16534  lcmfn0val  16562  pcgcd  16813  pcmptcl  16826  pcmpt  16827  pcmpt2  16828  pcprod  16830  fldivp1  16832  prmreclem2  16852  prmreclem4  16854  vdwlem6  16921  prmop1  16973  fvprmselelfz  16979  fvprmselgcd1  16980  ressval2  17180  xpsaddlem  17521  xpsvsca  17525  mreexexd  17594  setcepi  18040  pmtrmvd  19326  fincygsubgodd  19984  obselocv  21289  mvrf1  21551  mplcoe3  21599  mplmon2  21628  psrbagsn  21630  evlslem1  21651  mhpsclcl  21696  mhpvarcl  21697  dmatmul  22006  1mavmul  22057  mulmarep1gsum2  22083  1marepvmarrepid  22084  mdetdiag  22108  mdetrsca2  22113  mdetrlin2  22116  mdetunilem5  22125  mdetunilem7  22127  mdetunilem8  22128  mdetunilem9  22129  mndifsplit  22145  maducoeval2  22149  madugsum  22152  madurid  22153  smadiadetglem2  22181  1elcpmat  22224  decpmatid  22279  ptpjpre1  23082  ptbasfi  23092  isfcls  23520  ptcmplem2  23564  ptcmplem3  23565  dscmet  24088  dscopn  24089  icccmplem2  24346  cnmpopc  24451  iccpnfcnv  24467  xrhmeo  24469  pcoval2  24539  pcopt  24545  pcopt2  24546  pcoass  24547  pcorevlem  24549  i1f1lem  25213  itg1addlem2  25221  itg1addlem3  25222  i1fres  25230  itg1climres  25239  mbfi1fseqlem4  25243  mbfi1fseqlem5  25244  itg2const2  25266  itg2seq  25267  itg2uba  25268  itg2splitlem  25273  itg2split  25274  itg2monolem1  25275  itg2gt0  25285  itg2cnlem1  25286  itg2cnlem2  25287  iblss  25329  iblss2  25330  itgle  25334  itgss  25336  ibladdlem  25344  itgaddlem1  25347  iblabslem  25352  iblabs  25353  iblabsr  25354  iblmulc2  25355  bddmulibl  25363  bddiblnc  25366  ditgneg  25381  elply2  25717  coeeq2  25763  dgrle  25764  coe1termlem  25779  logcnlem3  26159  igamgam  26560  isppw  26625  isnsqf  26646  mule1  26659  sqff1o  26693  chtublem  26721  dchrelbasd  26749  bposlem1  26794  bposlem3  26796  bposlem5  26798  bposlem6  26799  lgsneg  26831  lgsdilem  26834  lgsdir2  26840  lgsdir  26842  lgsdi  26844  lgsne0  26845  gausslemma2dlem1a  26875  2lgslem1c  26903  2lgs  26917  dchrvmasum2if  27007  ostth2lem4  27146  nosupno  27213  nosupdm  27214  nosupbday  27215  nosupfv  27216  nosupres  27217  nosupbnd1lem1  27218  noinfno  27228  noinfdm  27229  noinffv  27231  maxs1  27275  maxs2  27276  mins1  27277  mins2  27278  axlowdimlem15  28252  elimifd  31813  elim2if  31814  ifeq3da  31816  ifnetrue  31817  imadifxp  31870  pmtridf1o  32294  resvval2  32484  xrge0iifcnv  32982  indval2  33081  ddeval0  33302  eulerpartlemb  33436  plymulx0  33627  signsw0glem  33633  signswmnd  33637  dfrdg2  34836  dfrdg3  34837  unisnif  34966  dfrdg4  34992  bj-xpima1sn  35923  finxpreclem2  36357  finxpreclem5  36362  matunitlindflem1  36570  poimirlem15  36589  poimirlem23  36597  mbfposadd  36621  itg2addnclem  36625  itg2addnclem3  36627  itg2gt0cn  36629  ibladdnclem  36630  itgaddnclem1  36632  iblabsnclem  36637  iblabsnc  36638  iblmulc2nc  36639  ftc1anclem5  36651  ftc1anclem7  36653  ftc1anclem8  36654  ftc1anc  36655  areacirclem5  36666  areacirc  36667  heiborlem4  36768  ac6s6  37126  riotaclbgBAD  37910  cdleme27a  39324  cdleme31sn2  39346  dihvalc  40190  mapdhval2  40683  hdmap1val2  40757  metakunt6  41076  metakunt7  41077  metakunt8  41078  metakunt11  41081  metakunt12  41082  metakunt22  41092  brif1  41127  brif2  41128  brif12  41129  fsuppind  41244  dffltz  41458  pw2f1ocnv  41858  aomclem5  41882  arearect  42046  areaquad  42047  safesnsupfidom1o  42250  safesnsupfilb  42251  upbdrech2  44097  lptioo2  44426  lptioo1  44427  limsupmnfuzlem  44521  limsupre3uzlem  44530  limsup10exlem  44567  coskpi2  44661  cosknegpi  44664  icccncfext  44682  cncfiooicclem1  44688  cncfiooiccre  44690  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  itgioocnicc  44772  iblcncfioo  44773  volico  44778  sublevolico  44779  voliooico  44787  voliccico  44794  dirkerper  44891  dirkertrigeq  44896  dirkercncflem2  44899  fourierdlem10  44912  fourierdlem32  44934  fourierdlem33  44935  fourierdlem37  44939  fourierdlem62  44963  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem79  44980  fourierdlem81  44982  fourierdlem82  44983  fourierdlem93  44994  fourierdlem97  44998  fourierdlem101  45002  fourierdlem103  45004  fourierdlem104  45005  sqwvfoura  45023  sqwvfourb  45024  fourierswlem  45025  fouriersw  45026  elaa2lem  45028  etransclem15  45044  etransclem19  45048  etransclem23  45052  etransclem24  45053  etransclem25  45054  ioorrnopnxrlem  45101  nnfoctbdjlem  45250  isomenndlem  45325  ovn0  45361  hsphoidmvle2  45380  hoidmv1lelem1  45386  hoidmv1lelem2  45387  hoidmv1le  45389  hoidmvlelem2  45391  hoidmvlelem3  45392  ovnhoilem1  45396  hspdifhsp  45411  hoidifhspdmvle  45415  hspmbllem1  45421  hspmbllem2  45422  hspmbl  45424  volico2  45436  ovolval4lem2  45445  ovolval5lem1  45447  afvnfundmuv  45926  ndfatafv2  45998  prproropf1olem4  46253  suppmptcfin  47134  linc1  47184  ifnmfalse  47886