Theorem iffalse 4476

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114  {cab 2715  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  iffalsei  4477  iffalsed  4478  ifnefalse  4479  iftrueb  4480  ifsb  4481  ifbi  4490  ifeq1da  4499  ifeq12da  4501  ifclda  4503  ifeqda  4504  elimif  4505  ifbothda  4506  ifid  4508  ifnot  4520  ifan  4521  ifor  4522  2if2  4523  ifcomnan  4524  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elimdhyp  4538  keephyp2v  4540  keephyp3v  4541  dfopif  4814  opprc  4840  somin1  6090  elimdelov  7456  brif1  7457  ovif12  7460  ifmpt2v  7462  oevn0  8443  pw2f1olem  9012  unxpdomlem2  9160  unxpdomlem3  9161  infsupprpr  9412  oi0  9436  wemaplem2  9455  ixpiunwdom  9498  cantnfp1lem3  9592  cantnflem1  9601  dfac12lem2  10058  fin23lem14  10246  axcc2lem  10349  ttukeylem5  10426  indval2  12155  uzin  12815  xrmax1  13118  xrmax2  13119  xrmin1  13120  xrmin2  13121  max1ALT  13129  ifle  13140  xmulneg1  13212  modifeq2int  13886  seqf1olem1  13994  seqf1olem2  13995  bcval3  14259  swrdccat  14688  pfxccat3a  14691  swrdccat3b  14693  repswswrd  14737  cshword  14744  ccatco  14788  sumrblem  15664  fsumcvg  15665  summolem2a  15668  sumss  15677  fsumcvg2  15680  sumsplit  15721  prodeq2ii  15867  prodrblem  15885  fprodcvg  15886  prodmolem2a  15890  zprod  15893  prodss  15903  ruclem2  16190  ruclem3  16191  flodddiv4  16375  sadadd2lem2  16410  sadcp1  16415  sadcaddlem  16417  gcdn0val  16458  dfgcd2  16506  lcmn0val  16555  lcmfn0val  16583  pcgcd  16840  pcmptcl  16853  pcmpt  16854  pcmpt2  16855  pcprod  16857  fldivp1  16859  prmreclem2  16879  prmreclem4  16881  vdwlem6  16948  prmop1  17000  fvprmselelfz  17006  fvprmselgcd1  17007  ressval2  17196  xpsaddlem  17528  xpsvsca  17532  mreexexd  17605  setcepi  18046  pmtrmvd  19422  fincygsubgodd  20080  obselocv  21718  mvrf1  21974  mplcoe3  22026  mplmon2  22049  psrbagsn  22051  evlslem1  22070  mhpsclcl  22123  mhpvarcl  22124  dmatmul  22472  1mavmul  22523  mulmarep1gsum2  22549  1marepvmarrepid  22550  mdetdiag  22574  mdetrsca2  22579  mdetrlin2  22582  mdetunilem5  22591  mdetunilem7  22593  mdetunilem8  22594  mdetunilem9  22595  mndifsplit  22611  maducoeval2  22615  madugsum  22618  madurid  22619  smadiadetglem2  22647  1elcpmat  22690  decpmatid  22745  ptpjpre1  23546  ptbasfi  23556  isfcls  23984  ptcmplem2  24028  ptcmplem3  24029  dscmet  24547  dscopn  24548  icccmplem2  24799  cnmpopc  24905  iccpnfcnv  24921  xrhmeo  24923  pcoval2  24993  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  i1f1lem  25666  itg1addlem2  25674  itg1addlem3  25675  i1fres  25682  itg1climres  25691  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  itg2const2  25718  itg2seq  25719  itg2uba  25720  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  iblss  25782  iblss2  25783  itgle  25787  itgss  25789  ibladdlem  25797  itgaddlem1  25800  iblabslem  25805  iblabs  25806  iblabsr  25807  iblmulc2  25808  bddmulibl  25816  bddiblnc  25819  ditgneg  25834  elply2  26171  coeeq2  26217  dgrle  26218  coe1termlem  26233  logcnlem3  26621  igamgam  27026  isppw  27091  isnsqf  27112  mule1  27125  sqff1o  27159  chtublem  27188  dchrelbasd  27216  bposlem1  27261  bposlem3  27263  bposlem5  27265  bposlem6  27266  lgsneg  27298  lgsdilem  27301  lgsdir2  27307  lgsdir  27309  lgsdi  27311  lgsne0  27312  gausslemma2dlem1a  27342  2lgslem1c  27370  2lgs  27384  dchrvmasum2if  27474  ostth2lem4  27613  nosupno  27681  nosupdm  27682  nosupbday  27683  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  noinfno  27696  noinfdm  27697  noinffv  27699  maxs1  27747  maxs2  27748  mins1  27749  mins2  27750  abssnid  28249  abssge0  28251  axlowdimlem15  29039  elimifd  32628  elim2if  32629  ifeq3da  32631  ifnetrue  32632  imadifxp  32686  pmtridf1o  33170  resvval2  33406  xrge0iifcnv  34093  ddeval0  34395  eulerpartlemb  34528  plymulx0  34707  signsw0glem  34713  signswmnd  34717  dfrdg2  35991  dfrdg3  35992  unisnif  36121  dfrdg4  36149  bj-xpima1sn  37279  finxpreclem2  37720  finxpreclem5  37725  matunitlindflem1  37951  poimirlem15  37970  poimirlem23  37978  mbfposadd  38002  itg2addnclem  38006  itg2addnclem3  38008  itg2gt0cn  38010  ibladdnclem  38011  itgaddnclem1  38013  iblabsnclem  38018  iblabsnc  38019  iblmulc2nc  38020  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  areacirclem5  38047  areacirc  38048  heiborlem4  38149  ac6s6  38507  riotaclbgBAD  39414  cdleme27a  40827  cdleme31sn2  40849  dihvalc  41693  mapdhval2  42186  hdmap1val2  42260  brif2  42679  brif12  42680  fsuppind  43037  dffltz  43081  pw2f1ocnv  43483  aomclem5  43504  arearect  43661  areaquad  43662  safesnsupfidom1o  43862  safesnsupfilb  43863  upbdrech2  45759  lptioo2  46079  lptioo1  46080  limsupmnfuzlem  46172  limsupre3uzlem  46181  limsup10exlem  46218  coskpi2  46312  cosknegpi  46315  icccncfext  46333  cncfiooicclem1  46339  cncfiooiccre  46341  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  itgioocnicc  46423  iblcncfioo  46424  volico  46429  sublevolico  46430  voliooico  46438  voliccico  46445  dirkerper  46542  dirkertrigeq  46547  dirkercncflem2  46550  fourierdlem10  46563  fourierdlem32  46585  fourierdlem33  46586  fourierdlem37  46590  fourierdlem62  46614  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem93  46645  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  elaa2lem  46679  etransclem15  46695  etransclem19  46699  etransclem23  46703  etransclem24  46704  etransclem25  46705  ioorrnopnxrlem  46752  nnfoctbdjlem  46901  isomenndlem  46976  ovn0  47012  hsphoidmvle2  47031  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1le  47040  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem1  47047  hspdifhsp  47062  hoidifhspdmvle  47066  hspmbllem1  47072  hspmbllem2  47073  hspmbl  47075  volico2  47087  ovolval4lem2  47096  ovolval5lem1  47098  afvnfundmuv  47599  ndfatafv2  47671  difmodm1lt  47825  prproropf1olem4  47978  suppmptcfin  48864  linc1  48913  discsubc  49551  oppfrcl3  49617  eloppf  49620  eloppf2  49621  ifnmfalse  50250