Theorem iffalse 4534

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108  {cab 2714  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  iffalsei  4535  iffalsed  4536  ifnefalse  4537  iftrueb  4538  ifsb  4539  ifbi  4548  ifeq1da  4557  ifeq12da  4559  ifclda  4561  ifeqda  4562  elimif  4563  ifbothda  4564  ifid  4566  ifnot  4578  ifan  4579  ifor  4580  2if2  4581  ifcomnan  4582  elimhyp  4591  elimhyp2v  4592  elimhyp3v  4593  elimhyp4v  4594  elimdhyp  4596  keephyp2v  4598  keephyp3v  4599  dfopif  4870  opprc  4896  somin1  6153  elimdelov  7529  brif1  7530  ovif12  7533  ifmpt2v  7535  oevn0  8553  pw2f1olem  9116  unxpdomlem2  9287  unxpdomlem3  9288  infsupprpr  9544  oi0  9568  wemaplem2  9587  ixpiunwdom  9630  cantnfp1lem3  9720  cantnflem1  9729  dfac12lem2  10185  fin23lem14  10373  axcc2lem  10476  ttukeylem5  10553  uzin  12918  xrmax1  13217  xrmax2  13218  xrmin1  13219  xrmin2  13220  max1ALT  13228  ifle  13239  xmulneg1  13311  modifeq2int  13974  seqf1olem1  14082  seqf1olem2  14083  bcval3  14345  swrdccat  14773  pfxccat3a  14776  swrdccat3b  14778  repswswrd  14822  cshword  14829  ccatco  14874  sumrblem  15747  fsumcvg  15748  summolem2a  15751  sumss  15760  fsumcvg2  15763  sumsplit  15804  prodeq2ii  15947  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  zprod  15973  prodss  15983  ruclem2  16268  ruclem3  16269  flodddiv4  16452  sadadd2lem2  16487  sadcp1  16492  sadcaddlem  16494  gcdn0val  16535  dfgcd2  16583  lcmn0val  16632  lcmfn0val  16660  pcgcd  16916  pcmptcl  16929  pcmpt  16930  pcmpt2  16931  pcprod  16933  fldivp1  16935  prmreclem2  16955  prmreclem4  16957  vdwlem6  17024  prmop1  17076  fvprmselelfz  17082  fvprmselgcd1  17083  ressval2  17279  xpsaddlem  17618  xpsvsca  17622  mreexexd  17691  setcepi  18133  pmtrmvd  19474  fincygsubgodd  20132  obselocv  21748  mvrf1  22006  mplcoe3  22056  mplmon2  22085  psrbagsn  22087  evlslem1  22106  mhpsclcl  22151  mhpvarcl  22152  dmatmul  22503  1mavmul  22554  mulmarep1gsum2  22580  1marepvmarrepid  22581  mdetdiag  22605  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  mdetunilem7  22624  mdetunilem8  22625  mdetunilem9  22626  mndifsplit  22642  maducoeval2  22646  madugsum  22649  madurid  22650  smadiadetglem2  22678  1elcpmat  22721  decpmatid  22776  ptpjpre1  23579  ptbasfi  23589  isfcls  24017  ptcmplem2  24061  ptcmplem3  24062  dscmet  24585  dscopn  24586  icccmplem2  24845  cnmpopc  24955  iccpnfcnv  24975  xrhmeo  24977  pcoval2  25049  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  i1f1lem  25724  itg1addlem2  25732  itg1addlem3  25733  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  itg2const2  25776  itg2seq  25777  itg2uba  25778  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  iblss2  25841  itgle  25845  itgss  25847  ibladdlem  25855  itgaddlem1  25858  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  bddmulibl  25874  bddiblnc  25877  ditgneg  25892  elply2  26235  coeeq2  26281  dgrle  26282  coe1termlem  26297  logcnlem3  26686  igamgam  27092  isppw  27157  isnsqf  27178  mule1  27191  sqff1o  27225  chtublem  27255  dchrelbasd  27283  bposlem1  27328  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgsneg  27365  lgsdilem  27368  lgsdir2  27374  lgsdir  27376  lgsdi  27378  lgsne0  27379  gausslemma2dlem1a  27409  2lgslem1c  27437  2lgs  27451  dchrvmasum2if  27541  ostth2lem4  27680  nosupno  27748  nosupdm  27749  nosupbday  27750  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  noinfno  27763  noinfdm  27764  noinffv  27766  maxs1  27810  maxs2  27811  mins1  27812  mins2  27813  abssnid  28267  abssge0  28269  axlowdimlem15  28971  elimifd  32556  elim2if  32557  ifeq3da  32559  ifnetrue  32560  imadifxp  32614  indval2  32839  pmtridf1o  33114  resvval2  33355  xrge0iifcnv  33932  ddeval0  34236  eulerpartlemb  34370  plymulx0  34562  signsw0glem  34568  signswmnd  34572  dfrdg2  35796  dfrdg3  35797  unisnif  35926  dfrdg4  35952  bj-xpima1sn  36957  finxpreclem2  37391  finxpreclem5  37396  matunitlindflem1  37623  poimirlem15  37642  poimirlem23  37650  mbfposadd  37674  itg2addnclem  37678  itg2addnclem3  37680  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem1  37685  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  areacirclem5  37719  areacirc  37720  heiborlem4  37821  ac6s6  38179  riotaclbgBAD  38955  cdleme27a  40369  cdleme31sn2  40391  dihvalc  41235  mapdhval2  41728  hdmap1val2  41802  metakunt6  42211  metakunt7  42212  metakunt8  42213  metakunt11  42216  metakunt12  42217  metakunt22  42227  brif2  42263  brif12  42264  fsuppind  42600  dffltz  42644  pw2f1ocnv  43049  aomclem5  43070  arearect  43227  areaquad  43228  safesnsupfidom1o  43430  safesnsupfilb  43431  upbdrech2  45320  lptioo2  45646  lptioo1  45647  limsupmnfuzlem  45741  limsupre3uzlem  45750  limsup10exlem  45787  coskpi2  45881  cosknegpi  45884  icccncfext  45902  cncfiooicclem1  45908  cncfiooiccre  45910  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  itgioocnicc  45992  iblcncfioo  45993  volico  45998  sublevolico  45999  voliooico  46007  voliccico  46014  dirkerper  46111  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem10  46132  fourierdlem32  46154  fourierdlem33  46155  fourierdlem37  46159  fourierdlem62  46183  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem93  46214  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  elaa2lem  46248  etransclem15  46264  etransclem19  46268  etransclem23  46272  etransclem24  46273  etransclem25  46274  ioorrnopnxrlem  46321  nnfoctbdjlem  46470  isomenndlem  46545  ovn0  46581  hsphoidmvle2  46600  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  hspdifhsp  46631  hoidifhspdmvle  46635  hspmbllem1  46641  hspmbllem2  46642  hspmbl  46644  volico2  46656  ovolval4lem2  46665  ovolval5lem1  46667  afvnfundmuv  47151  ndfatafv2  47223  prproropf1olem4  47493  suppmptcfin  48292  linc1  48342  ifnmfalse  49282