Theorem iffalse 4434

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 847   = wceq 1543   ∈ wcel 2112  {cab 2714  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-if 4426

This theorem is referenced by:  iffalsei  4435  iffalsed  4436  ifnefalse  4437  ifsb  4438  ifbi  4447  ifeq1da  4456  ifeq12da  4458  ifclda  4460  ifeqda  4461  elimif  4462  ifbothda  4463  ifid  4465  ifnot  4477  ifan  4478  ifor  4479  2if2  4480  ifcomnan  4481  elimhyp  4490  elimhyp2v  4491  elimhyp3v  4492  elimhyp4v  4493  elimdhyp  4495  keephyp2v  4497  keephyp3v  4498  dfopifOLD  4767  opprc  4793  somin1  5978  elimdelov  7285  ovif12  7288  oevn0  8220  pw2f1olem  8727  unxpdomlem2  8859  unxpdomlem3  8860  infsupprpr  9098  oi0  9122  wemaplem2  9141  ixpiunwdom  9184  cantnfp1lem3  9273  cantnflem1  9282  dfac12lem2  9723  fin23lem14  9912  axcc2lem  10015  ttukeylem5  10092  uzin  12439  xrmax1  12730  xrmax2  12731  xrmin1  12732  xrmin2  12733  max1ALT  12741  ifle  12752  xmulneg1  12824  modifeq2int  13471  seqf1olem1  13580  seqf1olem2  13581  bcval3  13837  swrdccat  14265  pfxccat3a  14268  swrdccat3b  14270  repswswrd  14314  cshword  14321  ccatco  14365  sumrblem  15240  fsumcvg  15241  summolem2a  15244  sumss  15253  fsumcvg2  15256  sumsplit  15295  prodeq2ii  15438  prodrblem  15454  fprodcvg  15455  prodmolem2a  15459  zprod  15462  prodss  15472  ruclem2  15756  ruclem3  15757  flodddiv4  15937  sadadd2lem2  15972  sadcp1  15977  sadcaddlem  15979  gcdn0val  16020  dfgcd2  16069  lcmn0val  16115  lcmfn0val  16143  pcgcd  16394  pcmptcl  16407  pcmpt  16408  pcmpt2  16409  pcprod  16411  fldivp1  16413  prmreclem2  16433  prmreclem4  16435  vdwlem6  16502  prmop1  16554  fvprmselelfz  16560  fvprmselgcd1  16561  ressval2  16737  xpsaddlem  17032  xpsvsca  17036  mreexexd  17105  setcepi  17548  pmtrmvd  18802  fincygsubgodd  19453  obselocv  20644  mvrf1  20904  mplcoe3  20949  mplmon2  20973  psrbagsn  20975  evlslem1  20996  mhpsclcl  21041  mhpvarcl  21042  dmatmul  21348  1mavmul  21399  mulmarep1gsum2  21425  1marepvmarrepid  21426  mdetdiag  21450  mdetrsca2  21455  mdetrlin2  21458  mdetunilem5  21467  mdetunilem7  21469  mdetunilem8  21470  mdetunilem9  21471  mndifsplit  21487  maducoeval2  21491  madugsum  21494  madurid  21495  smadiadetglem2  21523  1elcpmat  21566  decpmatid  21621  ptpjpre1  22422  ptbasfi  22432  isfcls  22860  ptcmplem2  22904  ptcmplem3  22905  dscmet  23424  dscopn  23425  icccmplem2  23674  cnmpopc  23779  iccpnfcnv  23795  xrhmeo  23797  pcoval2  23867  pcopt  23873  pcopt2  23874  pcoass  23875  pcorevlem  23877  i1f1lem  24540  itg1addlem2  24548  itg1addlem3  24549  i1fres  24557  itg1climres  24566  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  itg2const2  24593  itg2seq  24594  itg2uba  24595  itg2splitlem  24600  itg2split  24601  itg2monolem1  24602  itg2gt0  24612  itg2cnlem1  24613  itg2cnlem2  24614  iblss  24656  iblss2  24657  itgle  24661  itgss  24663  ibladdlem  24671  itgaddlem1  24674  iblabslem  24679  iblabs  24680  iblabsr  24681  iblmulc2  24682  bddmulibl  24690  bddiblnc  24693  ditgneg  24708  elply2  25044  coeeq2  25090  dgrle  25091  coe1termlem  25106  logcnlem3  25486  igamgam  25885  isppw  25950  isnsqf  25971  mule1  25984  sqff1o  26018  chtublem  26046  dchrelbasd  26074  bposlem1  26119  bposlem3  26121  bposlem5  26123  bposlem6  26124  lgsneg  26156  lgsdilem  26159  lgsdir2  26165  lgsdir  26167  lgsdi  26169  lgsne0  26170  gausslemma2dlem1a  26200  2lgslem1c  26228  2lgs  26242  dchrvmasum2if  26332  ostth2lem4  26471  axlowdimlem15  27001  elimifd  30559  elim2if  30560  ifeq3da  30562  imadifxp  30613  pmtridf1o  31034  resvval2  31201  xrge0iifcnv  31551  indval2  31648  ddeval0  31869  eulerpartlemb  32001  plymulx0  32192  signsw0glem  32198  signswmnd  32202  dfrdg2  33441  dfrdg3  33442  nosupno  33592  nosupdm  33593  nosupbday  33594  nosupfv  33595  nosupres  33596  nosupbnd1lem1  33597  noinfno  33607  noinfdm  33608  noinffv  33610  unisnif  33913  dfrdg4  33939  bj-xpima1sn  34832  finxpreclem2  35247  finxpreclem5  35252  matunitlindflem1  35459  poimirlem15  35478  poimirlem23  35486  mbfposadd  35510  itg2addnclem  35514  itg2addnclem3  35516  itg2gt0cn  35518  ibladdnclem  35519  itgaddnclem1  35521  iblabsnclem  35526  iblabsnc  35527  iblmulc2nc  35528  ftc1anclem5  35540  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  areacirclem5  35555  areacirc  35556  heiborlem4  35658  ac6s6  36016  riotaclbgBAD  36654  cdleme27a  38067  cdleme31sn2  38089  dihvalc  38933  mapdhval2  39426  hdmap1val2  39500  metakunt6  39793  metakunt7  39794  metakunt8  39795  metakunt11  39798  metakunt12  39799  metakunt22  39809  brif1  39852  brif2  39853  brif12  39854  fsuppind  39930  dffltz  40115  pw2f1ocnv  40503  aomclem5  40527  arearect  40690  areaquad  40691  upbdrech2  42461  lptioo2  42790  lptioo1  42791  limsupmnfuzlem  42885  limsupre3uzlem  42894  limsup10exlem  42931  coskpi2  43025  cosknegpi  43028  icccncfext  43046  cncfiooicclem1  43052  cncfiooiccre  43054  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  itgioocnicc  43136  iblcncfioo  43137  volico  43142  sublevolico  43143  voliooico  43151  voliccico  43158  dirkerper  43255  dirkertrigeq  43260  dirkercncflem2  43263  fourierdlem10  43276  fourierdlem32  43298  fourierdlem33  43299  fourierdlem37  43303  fourierdlem62  43327  fourierdlem73  43338  fourierdlem74  43339  fourierdlem75  43340  fourierdlem79  43344  fourierdlem81  43346  fourierdlem82  43347  fourierdlem93  43358  fourierdlem97  43362  fourierdlem101  43366  fourierdlem103  43368  fourierdlem104  43369  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  fouriersw  43390  elaa2lem  43392  etransclem15  43408  etransclem19  43412  etransclem23  43416  etransclem24  43417  etransclem25  43418  ioorrnopnxrlem  43465  nnfoctbdjlem  43611  isomenndlem  43686  ovn0  43722  hsphoidmvle2  43741  hoidmv1lelem1  43747  hoidmv1lelem2  43748  hoidmv1le  43750  hoidmvlelem2  43752  hoidmvlelem3  43753  ovnhoilem1  43757  hspdifhsp  43772  hoidifhspdmvle  43776  hspmbllem1  43782  hspmbllem2  43783  hspmbl  43785  volico2  43797  ovolval4lem2  43806  ovolval5lem1  43808  afvnfundmuv  44246  ndfatafv2  44318  prproropf1olem4  44574  suppmptcfin  45331  linc1  45382  ifnmfalse  46079