Theorem iffalse 4473

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1541   ∈ wcel 2109  {cab 2716  ifcif 4464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4465

This theorem is referenced by:  iffalsei  4474  iffalsed  4475  ifnefalse  4476  ifsb  4477  ifbi  4486  ifeq1da  4495  ifeq12da  4497  ifclda  4499  ifeqda  4500  elimif  4501  ifbothda  4502  ifid  4504  ifnot  4516  ifan  4517  ifor  4518  2if2  4519  ifcomnan  4520  elimhyp  4529  elimhyp2v  4530  elimhyp3v  4531  elimhyp4v  4532  elimdhyp  4534  keephyp2v  4536  keephyp3v  4537  dfopifOLD  4806  opprc  4832  somin1  6035  elimdelov  7362  ovif12  7365  oevn0  8321  pw2f1olem  8832  unxpdomlem2  8989  unxpdomlem3  8990  infsupprpr  9224  oi0  9248  wemaplem2  9267  ixpiunwdom  9310  cantnfp1lem3  9399  cantnflem1  9408  dfac12lem2  9884  fin23lem14  10073  axcc2lem  10176  ttukeylem5  10253  uzin  12600  xrmax1  12891  xrmax2  12892  xrmin1  12893  xrmin2  12894  max1ALT  12902  ifle  12913  xmulneg1  12985  modifeq2int  13634  seqf1olem1  13743  seqf1olem2  13744  bcval3  14001  swrdccat  14429  pfxccat3a  14432  swrdccat3b  14434  repswswrd  14478  cshword  14485  ccatco  14529  sumrblem  15404  fsumcvg  15405  summolem2a  15408  sumss  15417  fsumcvg2  15420  sumsplit  15461  prodeq2ii  15604  prodrblem  15620  fprodcvg  15621  prodmolem2a  15625  zprod  15628  prodss  15638  ruclem2  15922  ruclem3  15923  flodddiv4  16103  sadadd2lem2  16138  sadcp1  16143  sadcaddlem  16145  gcdn0val  16186  dfgcd2  16235  lcmn0val  16281  lcmfn0val  16309  pcgcd  16560  pcmptcl  16573  pcmpt  16574  pcmpt2  16575  pcprod  16577  fldivp1  16579  prmreclem2  16599  prmreclem4  16601  vdwlem6  16668  prmop1  16720  fvprmselelfz  16726  fvprmselgcd1  16727  ressval2  16927  xpsaddlem  17265  xpsvsca  17269  mreexexd  17338  setcepi  17784  pmtrmvd  19045  fincygsubgodd  19696  obselocv  20916  mvrf1  21175  mplcoe3  21220  mplmon2  21250  psrbagsn  21252  evlslem1  21273  mhpsclcl  21318  mhpvarcl  21319  dmatmul  21627  1mavmul  21678  mulmarep1gsum2  21704  1marepvmarrepid  21705  mdetdiag  21729  mdetrsca2  21734  mdetrlin2  21737  mdetunilem5  21746  mdetunilem7  21748  mdetunilem8  21749  mdetunilem9  21750  mndifsplit  21766  maducoeval2  21770  madugsum  21773  madurid  21774  smadiadetglem2  21802  1elcpmat  21845  decpmatid  21900  ptpjpre1  22703  ptbasfi  22713  isfcls  23141  ptcmplem2  23185  ptcmplem3  23186  dscmet  23709  dscopn  23710  icccmplem2  23967  cnmpopc  24072  iccpnfcnv  24088  xrhmeo  24090  pcoval2  24160  pcopt  24166  pcopt2  24167  pcoass  24168  pcorevlem  24170  i1f1lem  24834  itg1addlem2  24842  itg1addlem3  24843  i1fres  24851  itg1climres  24860  mbfi1fseqlem4  24864  mbfi1fseqlem5  24865  itg2const2  24887  itg2seq  24888  itg2uba  24889  itg2splitlem  24894  itg2split  24895  itg2monolem1  24896  itg2gt0  24906  itg2cnlem1  24907  itg2cnlem2  24908  iblss  24950  iblss2  24951  itgle  24955  itgss  24957  ibladdlem  24965  itgaddlem1  24968  iblabslem  24973  iblabs  24974  iblabsr  24975  iblmulc2  24976  bddmulibl  24984  bddiblnc  24987  ditgneg  25002  elply2  25338  coeeq2  25384  dgrle  25385  coe1termlem  25400  logcnlem3  25780  igamgam  26179  isppw  26244  isnsqf  26265  mule1  26278  sqff1o  26312  chtublem  26340  dchrelbasd  26368  bposlem1  26413  bposlem3  26415  bposlem5  26417  bposlem6  26418  lgsneg  26450  lgsdilem  26453  lgsdir2  26459  lgsdir  26461  lgsdi  26463  lgsne0  26464  gausslemma2dlem1a  26494  2lgslem1c  26522  2lgs  26536  dchrvmasum2if  26626  ostth2lem4  26765  axlowdimlem15  27305  elimifd  30865  elim2if  30866  ifeq3da  30868  imadifxp  30919  pmtridf1o  31340  resvval2  31507  xrge0iifcnv  31862  indval2  31961  ddeval0  32182  eulerpartlemb  32314  plymulx0  32505  signsw0glem  32511  signswmnd  32515  dfrdg2  33750  dfrdg3  33751  nosupno  33885  nosupdm  33886  nosupbday  33887  nosupfv  33888  nosupres  33889  nosupbnd1lem1  33890  noinfno  33900  noinfdm  33901  noinffv  33903  unisnif  34206  dfrdg4  34232  bj-xpima1sn  35125  finxpreclem2  35540  finxpreclem5  35545  matunitlindflem1  35752  poimirlem15  35771  poimirlem23  35779  mbfposadd  35803  itg2addnclem  35807  itg2addnclem3  35809  itg2gt0cn  35811  ibladdnclem  35812  itgaddnclem1  35814  iblabsnclem  35819  iblabsnc  35820  iblmulc2nc  35821  ftc1anclem5  35833  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837  areacirclem5  35848  areacirc  35849  heiborlem4  35951  ac6s6  36309  riotaclbgBAD  36947  cdleme27a  38360  cdleme31sn2  38382  dihvalc  39226  mapdhval2  39719  hdmap1val2  39793  metakunt6  40110  metakunt7  40111  metakunt8  40112  metakunt11  40115  metakunt12  40116  metakunt22  40126  brif1  40178  brif2  40179  brif12  40180  fsuppind  40259  dffltz  40451  pw2f1ocnv  40839  aomclem5  40863  arearect  41026  areaquad  41027  upbdrech2  42801  lptioo2  43126  lptioo1  43127  limsupmnfuzlem  43221  limsupre3uzlem  43230  limsup10exlem  43267  coskpi2  43361  cosknegpi  43364  icccncfext  43382  cncfiooicclem1  43388  cncfiooiccre  43390  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  itgioocnicc  43472  iblcncfioo  43473  volico  43478  sublevolico  43479  voliooico  43487  voliccico  43494  dirkerper  43591  dirkertrigeq  43596  dirkercncflem2  43599  fourierdlem10  43612  fourierdlem32  43634  fourierdlem33  43635  fourierdlem37  43639  fourierdlem62  43663  fourierdlem73  43674  fourierdlem74  43675  fourierdlem75  43676  fourierdlem79  43680  fourierdlem81  43682  fourierdlem82  43683  fourierdlem93  43694  fourierdlem97  43698  fourierdlem101  43702  fourierdlem103  43704  fourierdlem104  43705  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  elaa2lem  43728  etransclem15  43744  etransclem19  43748  etransclem23  43752  etransclem24  43753  etransclem25  43754  ioorrnopnxrlem  43801  nnfoctbdjlem  43947  isomenndlem  44022  ovn0  44058  hsphoidmvle2  44077  hoidmv1lelem1  44083  hoidmv1lelem2  44084  hoidmv1le  44086  hoidmvlelem2  44088  hoidmvlelem3  44089  ovnhoilem1  44093  hspdifhsp  44108  hoidifhspdmvle  44112  hspmbllem1  44118  hspmbllem2  44119  hspmbl  44121  volico2  44133  ovolval4lem2  44142  ovolval5lem1  44144  afvnfundmuv  44582  ndfatafv2  44654  prproropf1olem4  44910  suppmptcfin  45667  linc1  45718  ifnmfalse  46417