Theorem iffalse 4474

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 845   = wceq 1539   ∈ wcel 2104  {cab 2713  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4466

This theorem is referenced by:  iffalsei  4475  iffalsed  4476  ifnefalse  4477  ifsb  4478  ifbi  4487  ifeq1da  4496  ifeq12da  4498  ifclda  4500  ifeqda  4501  elimif  4502  ifbothda  4503  ifid  4505  ifnot  4517  ifan  4518  ifor  4519  2if2  4520  ifcomnan  4521  elimhyp  4530  elimhyp2v  4531  elimhyp3v  4532  elimhyp4v  4533  elimdhyp  4535  keephyp2v  4537  keephyp3v  4538  dfopif  4806  opprc  4832  somin1  6053  elimdelov  7403  ovif12  7406  oevn0  8376  pw2f1olem  8901  unxpdomlem2  9072  unxpdomlem3  9073  infsupprpr  9307  oi0  9331  wemaplem2  9350  ixpiunwdom  9393  cantnfp1lem3  9482  cantnflem1  9491  dfac12lem2  9946  fin23lem14  10135  axcc2lem  10238  ttukeylem5  10315  uzin  12664  xrmax1  12955  xrmax2  12956  xrmin1  12957  xrmin2  12958  max1ALT  12966  ifle  12977  xmulneg1  13049  modifeq2int  13699  seqf1olem1  13808  seqf1olem2  13809  bcval3  14066  swrdccat  14493  pfxccat3a  14496  swrdccat3b  14498  repswswrd  14542  cshword  14549  ccatco  14593  sumrblem  15468  fsumcvg  15469  summolem2a  15472  sumss  15481  fsumcvg2  15484  sumsplit  15525  prodeq2ii  15668  prodrblem  15684  fprodcvg  15685  prodmolem2a  15689  zprod  15692  prodss  15702  ruclem2  15986  ruclem3  15987  flodddiv4  16167  sadadd2lem2  16202  sadcp1  16207  sadcaddlem  16209  gcdn0val  16250  dfgcd2  16299  lcmn0val  16345  lcmfn0val  16373  pcgcd  16624  pcmptcl  16637  pcmpt  16638  pcmpt2  16639  pcprod  16641  fldivp1  16643  prmreclem2  16663  prmreclem4  16665  vdwlem6  16732  prmop1  16784  fvprmselelfz  16790  fvprmselgcd1  16791  ressval2  16991  xpsaddlem  17329  xpsvsca  17333  mreexexd  17402  setcepi  17848  pmtrmvd  19109  fincygsubgodd  19760  obselocv  20980  mvrf1  21239  mplcoe3  21284  mplmon2  21314  psrbagsn  21316  evlslem1  21337  mhpsclcl  21382  mhpvarcl  21383  dmatmul  21691  1mavmul  21742  mulmarep1gsum2  21768  1marepvmarrepid  21769  mdetdiag  21793  mdetrsca2  21798  mdetrlin2  21801  mdetunilem5  21810  mdetunilem7  21812  mdetunilem8  21813  mdetunilem9  21814  mndifsplit  21830  maducoeval2  21834  madugsum  21837  madurid  21838  smadiadetglem2  21866  1elcpmat  21909  decpmatid  21964  ptpjpre1  22767  ptbasfi  22777  isfcls  23205  ptcmplem2  23249  ptcmplem3  23250  dscmet  23773  dscopn  23774  icccmplem2  24031  cnmpopc  24136  iccpnfcnv  24152  xrhmeo  24154  pcoval2  24224  pcopt  24230  pcopt2  24231  pcoass  24232  pcorevlem  24234  i1f1lem  24898  itg1addlem2  24906  itg1addlem3  24907  i1fres  24915  itg1climres  24924  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  itg2const2  24951  itg2seq  24952  itg2uba  24953  itg2splitlem  24958  itg2split  24959  itg2monolem1  24960  itg2gt0  24970  itg2cnlem1  24971  itg2cnlem2  24972  iblss  25014  iblss2  25015  itgle  25019  itgss  25021  ibladdlem  25029  itgaddlem1  25032  iblabslem  25037  iblabs  25038  iblabsr  25039  iblmulc2  25040  bddmulibl  25048  bddiblnc  25051  ditgneg  25066  elply2  25402  coeeq2  25448  dgrle  25449  coe1termlem  25464  logcnlem3  25844  igamgam  26243  isppw  26308  isnsqf  26329  mule1  26342  sqff1o  26376  chtublem  26404  dchrelbasd  26432  bposlem1  26477  bposlem3  26479  bposlem5  26481  bposlem6  26482  lgsneg  26514  lgsdilem  26517  lgsdir2  26523  lgsdir  26525  lgsdi  26527  lgsne0  26528  gausslemma2dlem1a  26558  2lgslem1c  26586  2lgs  26600  dchrvmasum2if  26690  ostth2lem4  26829  axlowdimlem15  27369  elimifd  30931  elim2if  30932  ifeq3da  30934  imadifxp  30985  pmtridf1o  31406  resvval2  31573  xrge0iifcnv  31928  indval2  32027  ddeval0  32248  eulerpartlemb  32380  plymulx0  32571  signsw0glem  32577  signswmnd  32581  dfrdg2  33816  dfrdg3  33817  nosupno  33951  nosupdm  33952  nosupbday  33953  nosupfv  33954  nosupres  33955  nosupbnd1lem1  33956  noinfno  33966  noinfdm  33967  noinffv  33969  unisnif  34272  dfrdg4  34298  bj-xpima1sn  35190  finxpreclem2  35605  finxpreclem5  35610  matunitlindflem1  35817  poimirlem15  35836  poimirlem23  35844  mbfposadd  35868  itg2addnclem  35872  itg2addnclem3  35874  itg2gt0cn  35876  ibladdnclem  35877  itgaddnclem1  35879  iblabsnclem  35884  iblabsnc  35885  iblmulc2nc  35886  ftc1anclem5  35898  ftc1anclem7  35900  ftc1anclem8  35901  ftc1anc  35902  areacirclem5  35913  areacirc  35914  heiborlem4  36016  ac6s6  36374  riotaclbgBAD  37010  cdleme27a  38423  cdleme31sn2  38445  dihvalc  39289  mapdhval2  39782  hdmap1val2  39856  metakunt6  40172  metakunt7  40173  metakunt8  40174  metakunt11  40177  metakunt12  40178  metakunt22  40188  brif1  40235  brif2  40236  brif12  40237  fsuppind  40316  dffltz  40508  pw2f1ocnv  40897  aomclem5  40921  arearect  41084  areaquad  41085  upbdrech2  42895  lptioo2  43221  lptioo1  43222  limsupmnfuzlem  43316  limsupre3uzlem  43325  limsup10exlem  43362  coskpi2  43456  cosknegpi  43459  icccncfext  43477  cncfiooicclem1  43483  cncfiooiccre  43485  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  itgioocnicc  43567  iblcncfioo  43568  volico  43573  sublevolico  43574  voliooico  43582  voliccico  43589  dirkerper  43686  dirkertrigeq  43691  dirkercncflem2  43694  fourierdlem10  43707  fourierdlem32  43729  fourierdlem33  43730  fourierdlem37  43734  fourierdlem62  43758  fourierdlem73  43769  fourierdlem74  43770  fourierdlem75  43771  fourierdlem79  43775  fourierdlem81  43777  fourierdlem82  43778  fourierdlem93  43789  fourierdlem97  43793  fourierdlem101  43797  fourierdlem103  43799  fourierdlem104  43800  sqwvfoura  43818  sqwvfourb  43819  fourierswlem  43820  fouriersw  43821  elaa2lem  43823  etransclem15  43839  etransclem19  43843  etransclem23  43847  etransclem24  43848  etransclem25  43849  ioorrnopnxrlem  43896  nnfoctbdjlem  44043  isomenndlem  44118  ovn0  44154  hsphoidmvle2  44173  hoidmv1lelem1  44179  hoidmv1lelem2  44180  hoidmv1le  44182  hoidmvlelem2  44184  hoidmvlelem3  44185  ovnhoilem1  44189  hspdifhsp  44204  hoidifhspdmvle  44208  hspmbllem1  44214  hspmbllem2  44215  hspmbl  44217  volico2  44229  ovolval4lem2  44238  ovolval5lem1  44240  afvnfundmuv  44689  ndfatafv2  44761  prproropf1olem4  45016  suppmptcfin  45773  linc1  45824  ifnmfalse  46523