Theorem iffalse 4491

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145  {cab 2739  ifcif 4482

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  iffalsei  4492  iffalsed  4493  ifnefalse  4494  iftrueb  4495  ifsb  4496  ifbi  4505  ifeq1da  4514  ifeq12da  4516  ifclda  4518  ifeqda  4519  elimif  4520  ifbothda  4521  ifid  4523  ifnot  4535  ifan  4536  ifor  4537  2if2  4538  ifcomnan  4539  elimhyp  4548  elimhyp2v  4549  elimhyp3v  4550  elimhyp4v  4551  elimdhyp  4553  keephyp2v  4555  keephyp3v  4556  dfopif  4830  opprc  4856  somin1  6125  elimdelov  7508  brif1  7509  ovif12  7512  ifmpt2v  7514  oevn0  8507  pw2f1olem  9084  unxpdomlem2  9232  unxpdomlem3  9233  infsupprpr  9482  oi0  9506  wemaplem2  9525  ixpiunwdom  9568  cantnfp1lem3  9665  cantnflem1  9674  dfac12lem2  10204  fin23lem14  10392  axcc2lem  10495  ttukeylem5  10572  indval2  12306  uzin  12982  xrmax1  13286  xrmax2  13287  xrmin1  13288  xrmin2  13289  max1ALT  13297  ifle  13308  xmulneg1  13380  modifeq2int  14056  seqf1olem1  14164  seqf1olem2  14165  bcval3  14430  swrdccat  14864  pfxccat3a  14867  swrdccat3b  14869  repswswrd  14915  cshword  14922  ccatco  14966  sumrblem  15857  fsumcvg  15858  summolem2a  15861  sumss  15870  fsumcvg2  15873  sumsplit  15914  prodeq2ii  16060  prodrblem  16076  fprodcvg  16077  prodmolem2a  16081  zprod  16084  prodss  16094  ruclem2  16380  ruclem3  16381  flodddiv4  16565  sadadd2lem2  16600  sadcp1  16605  sadcaddlem  16607  gcdn0val  16648  dfgcd2  16699  lcmn0val  16750  lcmfn0val  16778  pcgcd  17036  pcmptcl  17049  pcmpt  17050  pcmpt2  17051  pcprod  17053  fldivp1  17055  prmreclem2  17075  prmreclem4  17077  vdwlem6  17144  prmop1  17196  fvprmselelfz  17202  fvprmselgcd1  17203  ressval2  17393  xpsaddlem  17725  xpsvsca  17729  mreexexd  17802  setcepi  18243  pmtrmvd  19650  fincygsubgodd  20308  obselocv  22014  mvrf1  22273  mplcoe3  22327  mplmon2  22350  psrbagsn  22352  evlslem1  22371  mhpsclcl  22448  mhpvarcl  22449  dmatmul  22792  1mavmul  22843  mulmarep1gsum2  22869  1marepvmarrepid  22870  mdetdiag  22894  mdetrsca2  22899  mdetrlin2  22902  mdetunilem5  22911  mdetunilem7  22913  mdetunilem8  22914  mdetunilem9  22915  mndifsplit  22931  maducoeval2  22935  madugsum  22938  madurid  22939  smadiadetglem2  22967  matunitlindflem1  22974  1elcpmat  23013  decpmatid  23068  ptpjpre1  23870  ptbasfi  23880  isfcls  24308  ptcmplem2  24352  ptcmplem3  24353  dscmet  24871  dscopn  24872  icccmplem2  25123  cnmpopc  25229  iccpnfcnv  25245  xrhmeo  25247  pcoval2  25317  pcopt  25323  pcopt2  25324  pcoass  25325  pcorevlem  25327  i1f1lem  25990  itg1addlem2  25998  itg1addlem3  25999  i1fres  26006  itg1climres  26015  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  itg2const2  26042  itg2seq  26043  itg2uba  26044  itg2splitlem  26049  itg2split  26050  itg2monolem1  26051  itg2gt0  26061  itg2cnlem1  26062  itg2cnlem2  26063  iblss  26105  iblss2  26106  itgle  26110  itgss  26112  ibladdlem  26120  itgaddlem1  26123  iblabslem  26128  iblabs  26129  iblabsr  26130  iblmulc2  26131  bddmulibl  26139  bddiblnc  26142  ditgneg  26157  elply2  26494  coeeq2  26541  dgrle  26542  coe1termlem  26557  plyn0mulidp  26584  logcnlem3  26954  igamgam  27358  isppw  27423  isnsqf  27444  mule1  27457  sqff1o  27491  chtublem  27520  dchrelbasd  27548  bposlem1  27593  bposlem3  27595  bposlem5  27597  bposlem6  27598  lgsneg  27630  lgsdilem  27633  lgsdir2  27639  lgsdir  27641  lgsdi  27643  lgsne0  27644  gausslemma2dlem1a  27674  2lgslem1c  27702  2lgs  27716  dchrvmasum2if  27806  ostth2lem4  27945  nosupno  28042  nosupdm  28043  nosupbday  28044  nosupfv  28045  nosupres  28046  nosupbnd1lem1  28047  noinfno  28057  noinfdm  28058  noinffv  28060  maxs1  28108  maxs2  28109  mins1  28110  mins2  28111  abssnid  28611  abssge0  28613  axlowdimlem15  29516  elimifd  33121  elim2if  33122  ifeq3da  33124  ifnetrue  33125  imadifxp  33177  pmtridf1o  33637  resvval2  33874  xrge0iifcnv  34547  ddeval0  34850  eulerpartlemb  34983  signsw0glem  35165  signswmnd  35169  vonf1oonfo  35867  dfrdg2  36527  dfrdg3  36528  unisnif  36657  dfrdg4  36685  bj-xpima1sn  37839  finxpreclem2  38281  finxpreclem5  38286  poimirlem15  38521  poimirlem23  38529  mbfposadd  38553  itg2addnclem  38557  itg2addnclem3  38559  itg2gt0cn  38561  ibladdnclem  38562  itgaddnclem1  38564  iblabsnclem  38569  iblabsnc  38570  iblmulc2nc  38571  ftc1anclem5  38583  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  areacirclem5  38598  areacirc  38599  heiborlem4  38716  ac6s6  39072  riotaclbgBAD  39979  cdleme27a  41392  cdleme31sn2  41414  dihvalc  42258  mapdhval2  42751  hdmap1val2  42825  brif2  43246  brif12  43247  fsuppind  43580  dffltz  43624  pw2f1ocnv  43997  aomclem5  44018  arearect  44175  areaquad  44176  safesnsupfidom1o  44376  safesnsupfilb  44377  upbdrech2  46267  lptioo2  46587  lptioo1  46588  limsupmnfuzlem  46680  limsupre3uzlem  46689  limsup10exlem  46726  coskpi2  46820  cosknegpi  46823  icccncfext  46841  cncfiooicclem1  46847  cncfiooiccre  46849  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  itgioocnicc  46931  iblcncfioo  46932  volico  46937  sublevolico  46938  voliooico  46946  voliccico  46953  dirkerper  47050  dirkertrigeq  47055  dirkercncflem2  47058  fourierdlem10  47071  fourierdlem32  47093  fourierdlem33  47094  fourierdlem37  47098  fourierdlem62  47122  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem79  47139  fourierdlem81  47141  fourierdlem82  47142  fourierdlem93  47153  fourierdlem97  47157  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  sqwvfoura  47182  sqwvfourb  47183  fourierswlem  47184  fouriersw  47185  elaa2lem  47187  etransclem15  47203  etransclem19  47207  etransclem23  47211  etransclem24  47212  etransclem25  47213  ioorrnopnxrlem  47260  nnfoctbdjlem  47409  isomenndlem  47484  ovn0  47520  hsphoidmvle2  47539  hoidmv1lelem1  47545  hoidmv1lelem2  47546  hoidmv1le  47548  hoidmvlelem2  47550  hoidmvlelem3  47551  ovnhoilem1  47555  hspdifhsp  47570  hoidifhspdmvle  47574  hspmbllem1  47580  hspmbllem2  47581  hspmbl  47583  volico2  47595  ovolval4lem2  47604  ovolval5lem1  47606  afvnfundmuv  48153  ndfatafv2  48225  difmodm1lt  48379  prproropf1olem4  48532  suppmptcfin  49432  linc1  49481  discsubc  50116  oppfrcl3  50182  eloppf  50185  eloppf2  50186  ifnmfalse  50803