Theorem iffalse 4481

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111  {cab 2709  ifcif 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4473

This theorem is referenced by:  iffalsei  4482  iffalsed  4483  ifnefalse  4484  iftrueb  4485  ifsb  4486  ifbi  4495  ifeq1da  4504  ifeq12da  4506  ifclda  4508  ifeqda  4509  elimif  4510  ifbothda  4511  ifid  4513  ifnot  4525  ifan  4526  ifor  4527  2if2  4528  ifcomnan  4529  elimhyp  4538  elimhyp2v  4539  elimhyp3v  4540  elimhyp4v  4541  elimdhyp  4543  keephyp2v  4545  keephyp3v  4546  dfopif  4819  opprc  4845  somin1  6079  elimdelov  7442  brif1  7443  ovif12  7446  ifmpt2v  7448  oevn0  8430  pw2f1olem  8994  unxpdomlem2  9141  unxpdomlem3  9142  infsupprpr  9390  oi0  9414  wemaplem2  9433  ixpiunwdom  9476  cantnfp1lem3  9570  cantnflem1  9579  dfac12lem2  10036  fin23lem14  10224  axcc2lem  10327  ttukeylem5  10404  uzin  12772  xrmax1  13074  xrmax2  13075  xrmin1  13076  xrmin2  13077  max1ALT  13085  ifle  13096  xmulneg1  13168  modifeq2int  13840  seqf1olem1  13948  seqf1olem2  13949  bcval3  14213  swrdccat  14642  pfxccat3a  14645  swrdccat3b  14647  repswswrd  14691  cshword  14698  ccatco  14742  sumrblem  15618  fsumcvg  15619  summolem2a  15622  sumss  15631  fsumcvg2  15634  sumsplit  15675  prodeq2ii  15818  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  zprod  15844  prodss  15854  ruclem2  16141  ruclem3  16142  flodddiv4  16326  sadadd2lem2  16361  sadcp1  16366  sadcaddlem  16368  gcdn0val  16409  dfgcd2  16457  lcmn0val  16506  lcmfn0val  16534  pcgcd  16790  pcmptcl  16803  pcmpt  16804  pcmpt2  16805  pcprod  16807  fldivp1  16809  prmreclem2  16829  prmreclem4  16831  vdwlem6  16898  prmop1  16950  fvprmselelfz  16956  fvprmselgcd1  16957  ressval2  17146  xpsaddlem  17477  xpsvsca  17481  mreexexd  17554  setcepi  17995  pmtrmvd  19368  fincygsubgodd  20026  obselocv  21665  mvrf1  21923  mplcoe3  21973  mplmon2  21996  psrbagsn  21998  evlslem1  22017  mhpsclcl  22062  mhpvarcl  22063  dmatmul  22412  1mavmul  22463  mulmarep1gsum2  22489  1marepvmarrepid  22490  mdetdiag  22514  mdetrsca2  22519  mdetrlin2  22522  mdetunilem5  22531  mdetunilem7  22533  mdetunilem8  22534  mdetunilem9  22535  mndifsplit  22551  maducoeval2  22555  madugsum  22558  madurid  22559  smadiadetglem2  22587  1elcpmat  22630  decpmatid  22685  ptpjpre1  23486  ptbasfi  23496  isfcls  23924  ptcmplem2  23968  ptcmplem3  23969  dscmet  24487  dscopn  24488  icccmplem2  24739  cnmpopc  24849  iccpnfcnv  24869  xrhmeo  24871  pcoval2  24943  pcopt  24949  pcopt2  24950  pcoass  24951  pcorevlem  24953  i1f1lem  25617  itg1addlem2  25625  itg1addlem3  25626  i1fres  25633  itg1climres  25642  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  itg2const2  25669  itg2seq  25670  itg2uba  25671  itg2splitlem  25676  itg2split  25677  itg2monolem1  25678  itg2gt0  25688  itg2cnlem1  25689  itg2cnlem2  25690  iblss  25733  iblss2  25734  itgle  25738  itgss  25740  ibladdlem  25748  itgaddlem1  25751  iblabslem  25756  iblabs  25757  iblabsr  25758  iblmulc2  25759  bddmulibl  25767  bddiblnc  25770  ditgneg  25785  elply2  26128  coeeq2  26174  dgrle  26175  coe1termlem  26190  logcnlem3  26580  igamgam  26986  isppw  27051  isnsqf  27072  mule1  27085  sqff1o  27119  chtublem  27149  dchrelbasd  27177  bposlem1  27222  bposlem3  27224  bposlem5  27226  bposlem6  27227  lgsneg  27259  lgsdilem  27262  lgsdir2  27268  lgsdir  27270  lgsdi  27272  lgsne0  27273  gausslemma2dlem1a  27303  2lgslem1c  27331  2lgs  27345  dchrvmasum2if  27435  ostth2lem4  27574  nosupno  27642  nosupdm  27643  nosupbday  27644  nosupfv  27645  nosupres  27646  nosupbnd1lem1  27647  noinfno  27657  noinfdm  27658  noinffv  27660  maxs1  27704  maxs2  27705  mins1  27706  mins2  27707  abssnid  28181  abssge0  28183  axlowdimlem15  28934  elimifd  32523  elim2if  32524  ifeq3da  32526  ifnetrue  32527  imadifxp  32581  indval2  32835  pmtridf1o  33063  resvval2  33296  xrge0iifcnv  33946  ddeval0  34248  eulerpartlemb  34381  plymulx0  34560  signsw0glem  34566  signswmnd  34570  dfrdg2  35837  dfrdg3  35838  unisnif  35967  dfrdg4  35995  bj-xpima1sn  37000  finxpreclem2  37434  finxpreclem5  37439  matunitlindflem1  37655  poimirlem15  37674  poimirlem23  37682  mbfposadd  37706  itg2addnclem  37710  itg2addnclem3  37712  itg2gt0cn  37714  ibladdnclem  37715  itgaddnclem1  37717  iblabsnclem  37722  iblabsnc  37723  iblmulc2nc  37724  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  areacirclem5  37751  areacirc  37752  heiborlem4  37853  ac6s6  38211  riotaclbgBAD  39052  cdleme27a  40465  cdleme31sn2  40487  dihvalc  41331  mapdhval2  41824  hdmap1val2  41898  brif2  42316  brif12  42317  fsuppind  42682  dffltz  42726  pw2f1ocnv  43129  aomclem5  43150  arearect  43307  areaquad  43308  safesnsupfidom1o  43509  safesnsupfilb  43510  upbdrech2  45408  lptioo2  45730  lptioo1  45731  limsupmnfuzlem  45823  limsupre3uzlem  45832  limsup10exlem  45869  coskpi2  45963  cosknegpi  45966  icccncfext  45984  cncfiooicclem1  45990  cncfiooiccre  45992  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  itgioocnicc  46074  iblcncfioo  46075  volico  46080  sublevolico  46081  voliooico  46089  voliccico  46096  dirkerper  46193  dirkertrigeq  46198  dirkercncflem2  46201  fourierdlem10  46214  fourierdlem32  46236  fourierdlem33  46237  fourierdlem37  46241  fourierdlem62  46265  fourierdlem73  46276  fourierdlem74  46277  fourierdlem75  46278  fourierdlem79  46282  fourierdlem81  46284  fourierdlem82  46285  fourierdlem93  46296  fourierdlem97  46300  fourierdlem101  46304  fourierdlem103  46306  fourierdlem104  46307  sqwvfoura  46325  sqwvfourb  46326  fourierswlem  46327  fouriersw  46328  elaa2lem  46330  etransclem15  46346  etransclem19  46350  etransclem23  46354  etransclem24  46355  etransclem25  46356  ioorrnopnxrlem  46403  nnfoctbdjlem  46552  isomenndlem  46627  ovn0  46663  hsphoidmvle2  46682  hoidmv1lelem1  46688  hoidmv1lelem2  46689  hoidmv1le  46691  hoidmvlelem2  46693  hoidmvlelem3  46694  ovnhoilem1  46698  hspdifhsp  46713  hoidifhspdmvle  46717  hspmbllem1  46723  hspmbllem2  46724  hspmbl  46726  volico2  46738  ovolval4lem2  46747  ovolval5lem1  46749  afvnfundmuv  47238  ndfatafv2  47310  difmodm1lt  47458  prproropf1olem4  47605  suppmptcfin  48475  linc1  48525  discsubc  49164  oppfrcl3  49230  eloppf  49233  eloppf2  49234  ifnmfalse  49863