Theorem iffalse 4539

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098  {cab 2702  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4531

This theorem is referenced by:  iffalsei  4540  iffalsed  4541  ifnefalse  4542  ifsb  4543  ifbi  4552  ifeq1da  4561  ifeq12da  4563  ifclda  4565  ifeqda  4566  elimif  4567  ifbothda  4568  ifid  4570  ifnot  4582  ifan  4583  ifor  4584  2if2  4585  ifcomnan  4586  elimhyp  4595  elimhyp2v  4596  elimhyp3v  4597  elimhyp4v  4598  elimdhyp  4600  keephyp2v  4602  keephyp3v  4603  dfopif  4872  opprc  4898  somin1  6140  elimdelov  7516  brif1  7517  ovif12  7520  oevn0  8536  pw2f1olem  9101  unxpdomlem2  9276  unxpdomlem3  9277  infsupprpr  9529  oi0  9553  wemaplem2  9572  ixpiunwdom  9615  cantnfp1lem3  9705  cantnflem1  9714  dfac12lem2  10169  fin23lem14  10358  axcc2lem  10461  ttukeylem5  10538  uzin  12895  xrmax1  13189  xrmax2  13190  xrmin1  13191  xrmin2  13192  max1ALT  13200  ifle  13211  xmulneg1  13283  modifeq2int  13934  seqf1olem1  14042  seqf1olem2  14043  bcval3  14301  swrdccat  14721  pfxccat3a  14724  swrdccat3b  14726  repswswrd  14770  cshword  14777  ccatco  14822  sumrblem  15693  fsumcvg  15694  summolem2a  15697  sumss  15706  fsumcvg2  15709  sumsplit  15750  prodeq2ii  15893  prodrblem  15909  fprodcvg  15910  prodmolem2a  15914  zprod  15917  prodss  15927  ruclem2  16212  ruclem3  16213  flodddiv4  16393  sadadd2lem2  16428  sadcp1  16433  sadcaddlem  16435  gcdn0val  16476  dfgcd2  16525  lcmn0val  16569  lcmfn0val  16597  pcgcd  16850  pcmptcl  16863  pcmpt  16864  pcmpt2  16865  pcprod  16867  fldivp1  16869  prmreclem2  16889  prmreclem4  16891  vdwlem6  16958  prmop1  17010  fvprmselelfz  17016  fvprmselgcd1  17017  ressval2  17217  xpsaddlem  17558  xpsvsca  17562  mreexexd  17631  setcepi  18080  pmtrmvd  19423  fincygsubgodd  20081  obselocv  21679  mvrf1  21948  mplcoe3  21998  mplmon2  22027  psrbagsn  22029  evlslem1  22050  mhpsclcl  22094  mhpvarcl  22095  dmatmul  22443  1mavmul  22494  mulmarep1gsum2  22520  1marepvmarrepid  22521  mdetdiag  22545  mdetrsca2  22550  mdetrlin2  22553  mdetunilem5  22562  mdetunilem7  22564  mdetunilem8  22565  mdetunilem9  22566  mndifsplit  22582  maducoeval2  22586  madugsum  22589  madurid  22590  smadiadetglem2  22618  1elcpmat  22661  decpmatid  22716  ptpjpre1  23519  ptbasfi  23529  isfcls  23957  ptcmplem2  24001  ptcmplem3  24002  dscmet  24525  dscopn  24526  icccmplem2  24783  cnmpopc  24893  iccpnfcnv  24913  xrhmeo  24915  pcoval2  24987  pcopt  24993  pcopt2  24994  pcoass  24995  pcorevlem  24997  i1f1lem  25662  itg1addlem2  25670  itg1addlem3  25671  i1fres  25679  itg1climres  25688  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  itg2const2  25715  itg2seq  25716  itg2uba  25717  itg2splitlem  25722  itg2split  25723  itg2monolem1  25724  itg2gt0  25734  itg2cnlem1  25735  itg2cnlem2  25736  iblss  25778  iblss2  25779  itgle  25783  itgss  25785  ibladdlem  25793  itgaddlem1  25796  iblabslem  25801  iblabs  25802  iblabsr  25803  iblmulc2  25804  bddmulibl  25812  bddiblnc  25815  ditgneg  25830  elply2  26175  coeeq2  26221  dgrle  26222  coe1termlem  26237  logcnlem3  26623  igamgam  27026  isppw  27091  isnsqf  27112  mule1  27125  sqff1o  27159  chtublem  27189  dchrelbasd  27217  bposlem1  27262  bposlem3  27264  bposlem5  27266  bposlem6  27267  lgsneg  27299  lgsdilem  27302  lgsdir2  27308  lgsdir  27310  lgsdi  27312  lgsne0  27313  gausslemma2dlem1a  27343  2lgslem1c  27371  2lgs  27385  dchrvmasum2if  27475  ostth2lem4  27614  nosupno  27682  nosupdm  27683  nosupbday  27684  nosupfv  27685  nosupres  27686  nosupbnd1lem1  27687  noinfno  27697  noinfdm  27698  noinffv  27700  maxs1  27744  maxs2  27745  mins1  27746  mins2  27747  abssnid  28187  abssge0  28189  axlowdimlem15  28839  elimifd  32413  elim2if  32414  ifeq3da  32416  ifnetrue  32417  imadifxp  32470  pmtridf1o  32907  resvval2  33139  xrge0iifcnv  33665  indval2  33764  ddeval0  33985  eulerpartlemb  34119  plymulx0  34310  signsw0glem  34316  signswmnd  34320  dfrdg2  35522  dfrdg3  35523  unisnif  35652  dfrdg4  35678  bj-xpima1sn  36566  finxpreclem2  37000  finxpreclem5  37005  matunitlindflem1  37220  poimirlem15  37239  poimirlem23  37247  mbfposadd  37271  itg2addnclem  37275  itg2addnclem3  37277  itg2gt0cn  37279  ibladdnclem  37280  itgaddnclem1  37282  iblabsnclem  37287  iblabsnc  37288  iblmulc2nc  37289  ftc1anclem5  37301  ftc1anclem7  37303  ftc1anclem8  37304  ftc1anc  37305  areacirclem5  37316  areacirc  37317  heiborlem4  37418  ac6s6  37776  riotaclbgBAD  38556  cdleme27a  39970  cdleme31sn2  39992  dihvalc  40836  mapdhval2  41329  hdmap1val2  41403  metakunt6  41796  metakunt7  41797  metakunt8  41798  metakunt11  41801  metakunt12  41802  metakunt22  41812  brif2  41846  brif12  41847  fsuppind  41958  dffltz  42193  pw2f1ocnv  42600  aomclem5  42624  arearect  42785  areaquad  42786  safesnsupfidom1o  42989  safesnsupfilb  42990  upbdrech2  44828  lptioo2  45157  lptioo1  45158  limsupmnfuzlem  45252  limsupre3uzlem  45261  limsup10exlem  45298  coskpi2  45392  cosknegpi  45395  icccncfext  45413  cncfiooicclem1  45419  cncfiooiccre  45421  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  itgioocnicc  45503  iblcncfioo  45504  volico  45509  sublevolico  45510  voliooico  45518  voliccico  45525  dirkerper  45622  dirkertrigeq  45627  dirkercncflem2  45630  fourierdlem10  45643  fourierdlem32  45665  fourierdlem33  45666  fourierdlem37  45670  fourierdlem62  45694  fourierdlem73  45705  fourierdlem74  45706  fourierdlem75  45707  fourierdlem79  45711  fourierdlem81  45713  fourierdlem82  45714  fourierdlem93  45725  fourierdlem97  45729  fourierdlem101  45733  fourierdlem103  45735  fourierdlem104  45736  sqwvfoura  45754  sqwvfourb  45755  fourierswlem  45756  fouriersw  45757  elaa2lem  45759  etransclem15  45775  etransclem19  45779  etransclem23  45783  etransclem24  45784  etransclem25  45785  ioorrnopnxrlem  45832  nnfoctbdjlem  45981  isomenndlem  46056  ovn0  46092  hsphoidmvle2  46111  hoidmv1lelem1  46117  hoidmv1lelem2  46118  hoidmv1le  46120  hoidmvlelem2  46122  hoidmvlelem3  46123  ovnhoilem1  46127  hspdifhsp  46142  hoidifhspdmvle  46146  hspmbllem1  46152  hspmbllem2  46153  hspmbl  46155  volico2  46167  ovolval4lem2  46176  ovolval5lem1  46178  afvnfundmuv  46657  ndfatafv2  46729  prproropf1olem4  46983  suppmptcfin  47629  linc1  47679  ifnmfalse  48380