Theorem iffalse 4490

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144  {cab 2738  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  iffalsei  4491  iffalsed  4492  ifnefalse  4493  iftrueb  4494  ifsb  4495  ifbi  4504  ifeq1da  4513  ifeq12da  4515  ifclda  4517  ifeqda  4518  elimif  4519  ifbothda  4520  ifid  4522  ifnot  4534  ifan  4535  ifor  4536  2if2  4537  ifcomnan  4538  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  dfopif  4836  opprc  4853  somin1  6126  elimdelov  7516  brif1  7517  ovif12  7520  ifmpt2v  7522  oevn0  8526  pw2f1olem  9103  unxpdomlem2  9251  unxpdomlem3  9252  infsupprpr  9501  oi0  9525  wemaplem2  9544  ixpiunwdom  9587  cantnfp1lem3  9684  cantnflem1  9693  dfac12lem2  10226  fin23lem14  10414  axcc2lem  10517  ttukeylem5  10594  indval2  12328  uzin  13004  xrmax1  13308  xrmax2  13309  xrmin1  13310  xrmin2  13311  max1ALT  13319  ifle  13330  xmulneg1  13402  modifeq2int  14079  seqf1olem1  14187  seqf1olem2  14188  bcval3  14453  swrdccat  14888  pfxccat3a  14891  swrdccat3b  14893  repswswrd  14939  cshword  14946  ccatco  14990  sumrblem  15882  fsumcvg  15883  summolem2a  15886  sumss  15895  fsumcvg2  15898  sumsplit  15939  prodeq2ii  16085  prodrblem  16101  fprodcvg  16102  prodmolem2a  16106  zprod  16109  prodss  16119  ruclem2  16405  ruclem3  16406  flodddiv4  16590  sadadd2lem2  16625  sadcp1  16630  sadcaddlem  16632  gcdn0val  16673  dfgcd2  16724  lcmn0val  16775  lcmfn0val  16803  pcgcd  17061  pcmptcl  17074  pcmpt  17075  pcmpt2  17076  pcprod  17078  fldivp1  17080  prmreclem2  17100  prmreclem4  17102  vdwlem6  17169  prmop1  17221  fvprmselelfz  17227  fvprmselgcd1  17228  ressval2  17418  xpsaddlem  17750  xpsvsca  17754  mreexexd  17827  setcepi  18268  pmtrmvd  19675  fincygsubgodd  20333  obselocv  22039  mvrf1  22298  mplcoe3  22352  mplmon2  22375  psrbagsn  22377  evlslem1  22396  mhpsclcl  22473  mhpvarcl  22474  dmatmul  22817  1mavmul  22868  mulmarep1gsum2  22894  1marepvmarrepid  22895  mdetdiag  22919  mdetrsca2  22924  mdetrlin2  22927  mdetunilem5  22936  mdetunilem7  22938  mdetunilem8  22939  mdetunilem9  22940  mndifsplit  22956  maducoeval2  22960  madugsum  22963  madurid  22964  smadiadetglem2  22992  matunitlindflem1  22999  1elcpmat  23038  decpmatid  23093  ptpjpre1  23895  ptbasfi  23905  isfcls  24333  ptcmplem2  24377  ptcmplem3  24378  dscmet  24896  dscopn  24897  icccmplem2  25148  cnmpopc  25254  iccpnfcnv  25270  xrhmeo  25272  pcoval2  25342  pcopt  25348  pcopt2  25349  pcoass  25350  pcorevlem  25352  i1f1lem  26015  itg1addlem2  26023  itg1addlem3  26024  i1fres  26031  itg1climres  26040  mbfi1fseqlem4  26044  mbfi1fseqlem5  26045  itg2const2  26067  itg2seq  26068  itg2uba  26069  itg2splitlem  26074  itg2split  26075  itg2monolem1  26076  itg2gt0  26086  itg2cnlem1  26087  itg2cnlem2  26088  iblss  26130  iblss2  26131  itgle  26135  itgss  26137  ibladdlem  26145  itgaddlem1  26148  iblabslem  26153  iblabs  26154  iblabsr  26155  iblmulc2  26156  bddmulibl  26164  bddiblnc  26167  ditgneg  26182  elply2  26519  coeeq2  26566  dgrle  26567  coe1termlem  26582  plyn0mulidp  26607  logcnlem3  26977  igamgam  27381  isppw  27446  isnsqf  27467  mule1  27480  sqff1o  27514  chtublem  27543  dchrelbasd  27571  bposlem1  27616  bposlem3  27618  bposlem5  27620  bposlem6  27621  lgsneg  27653  lgsdilem  27656  lgsdir2  27662  lgsdir  27664  lgsdi  27666  lgsne0  27667  gausslemma2dlem1a  27697  2lgslem1c  27725  2lgs  27739  dchrvmasum2if  27829  ostth2lem4  27968  nosupno  28065  nosupdm  28066  nosupbday  28067  nosupfv  28068  nosupres  28069  nosupbnd1lem1  28070  noinfno  28080  noinfdm  28081  noinffv  28083  maxs1  28131  maxs2  28132  mins1  28133  mins2  28134  abssnid  28634  abssge0  28636  axlowdimlem15  29539  elimifd  33186  elim2if  33187  ifeq3da  33189  ifnetrue  33190  imadifxp  33242  pmtridf1o  33701  resvval2  33938  xrge0iifcnv  34611  ddeval0  34914  eulerpartlemb  35046  signsw0glem  35228  signswmnd  35232  jaeqifi  35758  ordunmax  35765  soinfdom  35768  vonf1oonfo  35968  onf1oracwevd  35971  onprcf1of1ord  35974  dfrdg2  36649  dfrdg3  36650  unisnif  36779  dfrdg4  36807  bj-xpima1sn  37961  finxpreclem2  38406  finxpreclem5  38411  poimirlem15  38646  poimirlem23  38654  mbfposadd  38678  itg2addnclem  38682  itg2addnclem3  38684  itg2gt0cn  38686  ibladdnclem  38687  itgaddnclem1  38689  iblabsnclem  38694  iblabsnc  38695  iblmulc2nc  38696  ftc1anclem5  38708  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  areacirclem5  38723  areacirc  38724  heiborlem4  38841  ac6s6  39197  riotaclbgBAD  40104  cdleme27a  41517  cdleme31sn2  41539  dihvalc  42383  mapdhval2  42876  hdmap1val2  42950  brif2  43371  brif12  43372  fsuppind  43711  dffltz  43763  pw2f1ocnv  44137  aomclem5  44153  arearect  44310  areaquad  44311  safesnsupfidom1o  44511  safesnsupfilb  44512  upbdrech2  46417  lptioo2  46736  lptioo1  46737  limsupmnfuzlem  46829  limsupre3uzlem  46838  limsup10exlem  46875  coskpi2  46969  cosknegpi  46972  icccncfext  46990  cncfiooicclem1  46996  cncfiooiccre  46998  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  itgioocnicc  47080  iblcncfioo  47081  volico  47086  sublevolico  47087  voliooico  47095  voliccico  47102  dirkerper  47199  dirkertrigeq  47204  dirkercncflem2  47207  fourierdlem10  47220  fourierdlem32  47242  fourierdlem33  47243  fourierdlem37  47247  fourierdlem62  47271  fourierdlem73  47282  fourierdlem74  47283  fourierdlem75  47284  fourierdlem79  47288  fourierdlem81  47290  fourierdlem82  47291  fourierdlem93  47302  fourierdlem97  47306  fourierdlem101  47310  fourierdlem103  47312  fourierdlem104  47313  sqwvfoura  47331  sqwvfourb  47332  fourierswlem  47333  fouriersw  47334  elaa2lem  47336  etransclem15  47352  etransclem19  47356  etransclem23  47360  etransclem24  47361  etransclem25  47362  ioorrnopnxrlem  47409  nnfoctbdjlem  47558  isomenndlem  47633  ovn0  47669  hsphoidmvle2  47688  hoidmv1lelem1  47694  hoidmv1lelem2  47695  hoidmv1le  47697  hoidmvlelem2  47699  hoidmvlelem3  47700  ovnhoilem1  47704  hspdifhsp  47719  hoidifhspdmvle  47723  hspmbllem1  47729  hspmbllem2  47730  hspmbl  47732  volico2  47744  ovolval4lem2  47753  ovolval5lem1  47755  afvnfundmuv  48302  ndfatafv2  48374  difmodm1lt  48528  prproropf1olem4  48681  suppmptcfin  49581  linc1  49630  discsubc  50271  oppfrcl3  50339  eloppf  50342  eloppf2  50343  ifnmfalse  51027