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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 858   = wceq 1559   ∈ wcel 2141  {cab 2739  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  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  4827  opprc  4853  somin1  6117  elimdelov  7488  brif1  7489  ovif12  7492  ifmpt2v  7494  oevn0  8479  pw2f1olem  9049  unxpdomlem2  9197  unxpdomlem3  9198  infsupprpr  9449  oi0  9473  wemaplem2  9492  ixpiunwdom  9535  cantnfp1lem3  9632  cantnflem1  9641  dfac12lem2  10098  fin23lem14  10287  axcc2lem  10390  ttukeylem5  10467  indval2  12197  uzin  12872  xrmax1  13175  xrmax2  13176  xrmin1  13177  xrmin2  13178  max1ALT  13186  ifle  13197  xmulneg1  13269  modifeq2int  13943  seqf1olem1  14051  seqf1olem2  14052  bcval3  14316  swrdccat  14745  pfxccat3a  14748  swrdccat3b  14750  repswswrd  14794  cshword  14801  ccatco  14845  sumrblem  15721  fsumcvg  15722  summolem2a  15725  sumss  15734  fsumcvg2  15737  sumsplit  15778  prodeq2ii  15924  prodrblem  15942  fprodcvg  15943  prodmolem2a  15947  zprod  15950  prodss  15960  ruclem2  16247  ruclem3  16248  flodddiv4  16432  sadadd2lem2  16467  sadcp1  16472  sadcaddlem  16474  gcdn0val  16515  dfgcd2  16563  lcmn0val  16612  lcmfn0val  16640  pcgcd  16897  pcmptcl  16910  pcmpt  16911  pcmpt2  16912  pcprod  16914  fldivp1  16916  prmreclem2  16936  prmreclem4  16938  vdwlem6  17005  prmop1  17057  fvprmselelfz  17063  fvprmselgcd1  17064  ressval2  17254  xpsaddlem  17586  xpsvsca  17590  mreexexd  17663  setcepi  18104  pmtrmvd  19479  fincygsubgodd  20137  obselocv  21760  mvrf1  22017  mplcoe3  22071  mplmon2  22094  psrbagsn  22096  evlslem1  22115  mhpsclcl  22192  mhpvarcl  22193  dmatmul  22537  1mavmul  22588  mulmarep1gsum2  22614  1marepvmarrepid  22615  mdetdiag  22639  mdetrsca2  22644  mdetrlin2  22647  mdetunilem5  22656  mdetunilem7  22658  mdetunilem8  22659  mdetunilem9  22660  mndifsplit  22676  maducoeval2  22680  madugsum  22683  madurid  22684  smadiadetglem2  22712  1elcpmat  22755  decpmatid  22810  ptpjpre1  23611  ptbasfi  23621  isfcls  24049  ptcmplem2  24093  ptcmplem3  24094  dscmet  24612  dscopn  24613  icccmplem2  24864  cnmpopc  24970  iccpnfcnv  24986  xrhmeo  24988  pcoval2  25058  pcopt  25064  pcopt2  25065  pcoass  25066  pcorevlem  25068  i1f1lem  25731  itg1addlem2  25739  itg1addlem3  25740  i1fres  25747  itg1climres  25756  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  itg2const2  25783  itg2seq  25784  itg2uba  25785  itg2splitlem  25790  itg2split  25791  itg2monolem1  25792  itg2gt0  25802  itg2cnlem1  25803  itg2cnlem2  25804  iblss  25847  iblss2  25848  itgle  25852  itgss  25854  ibladdlem  25862  itgaddlem1  25865  iblabslem  25870  iblabs  25871  iblabsr  25872  iblmulc2  25873  bddmulibl  25881  bddiblnc  25884  ditgneg  25899  elply2  26236  coeeq2  26282  dgrle  26283  coe1termlem  26298  logcnlem3  26686  igamgam  27090  isppw  27155  isnsqf  27176  mule1  27189  sqff1o  27223  chtublem  27252  dchrelbasd  27280  bposlem1  27325  bposlem3  27327  bposlem5  27329  bposlem6  27330  lgsneg  27362  lgsdilem  27365  lgsdir2  27371  lgsdir  27373  lgsdi  27375  lgsne0  27376  gausslemma2dlem1a  27406  2lgslem1c  27434  2lgs  27448  dchrvmasum2if  27538  ostth2lem4  27677  nosupno  27744  nosupdm  27745  nosupbday  27746  nosupfv  27747  nosupres  27748  nosupbnd1lem1  27749  noinfno  27759  noinfdm  27760  noinffv  27762  maxs1  27810  maxs2  27811  mins1  27812  mins2  27813  abssnid  28313  abssge0  28315  axlowdimlem15  29103  elimifd  32691  elim2if  32692  ifeq3da  32694  ifnetrue  32695  imadifxp  32750  pmtridf1o  33235  resvval2  33478  xrge0iifcnv  34191  ddeval0  34493  eulerpartlemb  34626  plymulx0  34805  signsw0glem  34811  signswmnd  34815  vonf1oonfo  35422  dfrdg2  36107  dfrdg3  36108  unisnif  36237  dfrdg4  36265  bj-xpima1sn  37405  finxpreclem2  37848  finxpreclem5  37853  matunitlindflem1  38079  poimirlem15  38098  poimirlem23  38106  mbfposadd  38130  itg2addnclem  38134  itg2addnclem3  38136  itg2gt0cn  38138  ibladdnclem  38139  itgaddnclem1  38141  iblabsnclem  38146  iblabsnc  38147  iblmulc2nc  38148  ftc1anclem5  38160  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  areacirclem5  38175  areacirc  38176  heiborlem4  38277  ac6s6  38635  riotaclbgBAD  39542  cdleme27a  40955  cdleme31sn2  40977  dihvalc  41821  mapdhval2  42314  hdmap1val2  42388  brif2  42807  brif12  42808  fsuppind  43136  dffltz  43180  pw2f1ocnv  43578  aomclem5  43599  arearect  43756  areaquad  43757  safesnsupfidom1o  43957  safesnsupfilb  43958  upbdrech2  45851  lptioo2  46171  lptioo1  46172  limsupmnfuzlem  46264  limsupre3uzlem  46273  limsup10exlem  46310  coskpi2  46404  cosknegpi  46407  icccncfext  46425  cncfiooicclem1  46431  cncfiooiccre  46433  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  itgioocnicc  46515  iblcncfioo  46516  volico  46521  sublevolico  46522  voliooico  46530  voliccico  46537  dirkerper  46634  dirkertrigeq  46639  dirkercncflem2  46642  fourierdlem10  46655  fourierdlem32  46677  fourierdlem33  46678  fourierdlem37  46682  fourierdlem62  46706  fourierdlem73  46717  fourierdlem74  46718  fourierdlem75  46719  fourierdlem79  46723  fourierdlem81  46725  fourierdlem82  46726  fourierdlem93  46737  fourierdlem97  46741  fourierdlem101  46745  fourierdlem103  46747  fourierdlem104  46748  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  elaa2lem  46771  etransclem15  46787  etransclem19  46791  etransclem23  46795  etransclem24  46796  etransclem25  46797  ioorrnopnxrlem  46844  nnfoctbdjlem  46993  isomenndlem  47068  ovn0  47104  hsphoidmvle2  47123  hoidmv1lelem1  47129  hoidmv1lelem2  47130  hoidmv1le  47132  hoidmvlelem2  47134  hoidmvlelem3  47135  ovnhoilem1  47139  hspdifhsp  47154  hoidifhspdmvle  47158  hspmbllem1  47164  hspmbllem2  47165  hspmbl  47167  volico2  47179  ovolval4lem2  47188  ovolval5lem1  47190  afvnfundmuv  47697  ndfatafv2  47769  difmodm1lt  47923  prproropf1olem4  48076  suppmptcfin  48962  linc1  49011  discsubc  49649  oppfrcl3  49715  eloppf  49718  eloppf2  49719  ifnmfalse  50348