Theorem iffalse 4488

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113  {cab 2714  ifcif 4479

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  iffalsei  4489  iffalsed  4490  ifnefalse  4491  iftrueb  4492  ifsb  4493  ifbi  4502  ifeq1da  4511  ifeq12da  4513  ifclda  4515  ifeqda  4516  elimif  4517  ifbothda  4518  ifid  4520  ifnot  4532  ifan  4533  ifor  4534  2if2  4535  ifcomnan  4536  elimhyp  4545  elimhyp2v  4546  elimhyp3v  4547  elimhyp4v  4548  elimdhyp  4550  keephyp2v  4552  keephyp3v  4553  dfopif  4826  opprc  4852  somin1  6090  elimdelov  7454  brif1  7455  ovif12  7458  ifmpt2v  7460  oevn0  8442  pw2f1olem  9009  unxpdomlem2  9157  unxpdomlem3  9158  infsupprpr  9409  oi0  9433  wemaplem2  9452  ixpiunwdom  9495  cantnfp1lem3  9589  cantnflem1  9598  dfac12lem2  10055  fin23lem14  10243  axcc2lem  10346  ttukeylem5  10423  uzin  12787  xrmax1  13090  xrmax2  13091  xrmin1  13092  xrmin2  13093  max1ALT  13101  ifle  13112  xmulneg1  13184  modifeq2int  13856  seqf1olem1  13964  seqf1olem2  13965  bcval3  14229  swrdccat  14658  pfxccat3a  14661  swrdccat3b  14663  repswswrd  14707  cshword  14714  ccatco  14758  sumrblem  15634  fsumcvg  15635  summolem2a  15638  sumss  15647  fsumcvg2  15650  sumsplit  15691  prodeq2ii  15834  prodrblem  15852  fprodcvg  15853  prodmolem2a  15857  zprod  15860  prodss  15870  ruclem2  16157  ruclem3  16158  flodddiv4  16342  sadadd2lem2  16377  sadcp1  16382  sadcaddlem  16384  gcdn0val  16425  dfgcd2  16473  lcmn0val  16522  lcmfn0val  16550  pcgcd  16806  pcmptcl  16819  pcmpt  16820  pcmpt2  16821  pcprod  16823  fldivp1  16825  prmreclem2  16845  prmreclem4  16847  vdwlem6  16914  prmop1  16966  fvprmselelfz  16972  fvprmselgcd1  16973  ressval2  17162  xpsaddlem  17494  xpsvsca  17498  mreexexd  17571  setcepi  18012  pmtrmvd  19385  fincygsubgodd  20043  obselocv  21683  mvrf1  21941  mplcoe3  21993  mplmon2  22016  psrbagsn  22018  evlslem1  22037  mhpsclcl  22090  mhpvarcl  22091  dmatmul  22441  1mavmul  22492  mulmarep1gsum2  22518  1marepvmarrepid  22519  mdetdiag  22543  mdetrsca2  22548  mdetrlin2  22551  mdetunilem5  22560  mdetunilem7  22562  mdetunilem8  22563  mdetunilem9  22564  mndifsplit  22580  maducoeval2  22584  madugsum  22587  madurid  22588  smadiadetglem2  22616  1elcpmat  22659  decpmatid  22714  ptpjpre1  23515  ptbasfi  23525  isfcls  23953  ptcmplem2  23997  ptcmplem3  23998  dscmet  24516  dscopn  24517  icccmplem2  24768  cnmpopc  24878  iccpnfcnv  24898  xrhmeo  24900  pcoval2  24972  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  i1f1lem  25646  itg1addlem2  25654  itg1addlem3  25655  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  itg2const2  25698  itg2seq  25699  itg2uba  25700  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  iblss  25762  iblss2  25763  itgle  25767  itgss  25769  ibladdlem  25777  itgaddlem1  25780  iblabslem  25785  iblabs  25786  iblabsr  25787  iblmulc2  25788  bddmulibl  25796  bddiblnc  25799  ditgneg  25814  elply2  26157  coeeq2  26203  dgrle  26204  coe1termlem  26219  logcnlem3  26609  igamgam  27015  isppw  27080  isnsqf  27101  mule1  27114  sqff1o  27148  chtublem  27178  dchrelbasd  27206  bposlem1  27251  bposlem3  27253  bposlem5  27255  bposlem6  27256  lgsneg  27288  lgsdilem  27291  lgsdir2  27297  lgsdir  27299  lgsdi  27301  lgsne0  27302  gausslemma2dlem1a  27332  2lgslem1c  27360  2lgs  27374  dchrvmasum2if  27464  ostth2lem4  27603  nosupno  27671  nosupdm  27672  nosupbday  27673  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  noinfno  27686  noinfdm  27687  noinffv  27689  maxs1  27737  maxs2  27738  mins1  27739  mins2  27740  abssnid  28239  abssge0  28241  axlowdimlem15  29029  elimifd  32618  elim2if  32619  ifeq3da  32621  ifnetrue  32622  imadifxp  32676  indval2  32933  pmtridf1o  33176  resvval2  33412  xrge0iifcnv  34090  ddeval0  34392  eulerpartlemb  34525  plymulx0  34704  signsw0glem  34710  signswmnd  34714  dfrdg2  35987  dfrdg3  35988  unisnif  36117  dfrdg4  36145  bj-xpima1sn  37157  finxpreclem2  37591  finxpreclem5  37596  matunitlindflem1  37813  poimirlem15  37832  poimirlem23  37840  mbfposadd  37864  itg2addnclem  37868  itg2addnclem3  37870  itg2gt0cn  37872  ibladdnclem  37873  itgaddnclem1  37875  iblabsnclem  37880  iblabsnc  37881  iblmulc2nc  37882  ftc1anclem5  37894  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  areacirclem5  37909  areacirc  37910  heiborlem4  38011  ac6s6  38369  riotaclbgBAD  39210  cdleme27a  40623  cdleme31sn2  40645  dihvalc  41489  mapdhval2  41982  hdmap1val2  42056  brif2  42476  brif12  42477  fsuppind  42829  dffltz  42873  pw2f1ocnv  43275  aomclem5  43296  arearect  43453  areaquad  43454  safesnsupfidom1o  43654  safesnsupfilb  43655  upbdrech2  45552  lptioo2  45873  lptioo1  45874  limsupmnfuzlem  45966  limsupre3uzlem  45975  limsup10exlem  46012  coskpi2  46106  cosknegpi  46109  icccncfext  46127  cncfiooicclem1  46133  cncfiooiccre  46135  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  itgioocnicc  46217  iblcncfioo  46218  volico  46223  sublevolico  46224  voliooico  46232  voliccico  46239  dirkerper  46336  dirkertrigeq  46341  dirkercncflem2  46344  fourierdlem10  46357  fourierdlem32  46379  fourierdlem33  46380  fourierdlem37  46384  fourierdlem62  46408  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem79  46425  fourierdlem81  46427  fourierdlem82  46428  fourierdlem93  46439  fourierdlem97  46443  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  elaa2lem  46473  etransclem15  46489  etransclem19  46493  etransclem23  46497  etransclem24  46498  etransclem25  46499  ioorrnopnxrlem  46546  nnfoctbdjlem  46695  isomenndlem  46770  ovn0  46806  hsphoidmvle2  46825  hoidmv1lelem1  46831  hoidmv1lelem2  46832  hoidmv1le  46834  hoidmvlelem2  46836  hoidmvlelem3  46837  ovnhoilem1  46841  hspdifhsp  46856  hoidifhspdmvle  46860  hspmbllem1  46866  hspmbllem2  46867  hspmbl  46869  volico2  46881  ovolval4lem2  46890  ovolval5lem1  46892  afvnfundmuv  47381  ndfatafv2  47453  difmodm1lt  47601  prproropf1olem4  47748  suppmptcfin  48618  linc1  48667  discsubc  49305  oppfrcl3  49371  eloppf  49374  eloppf2  49375  ifnmfalse  50004