Theorem iffalse 4475

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  iffalsei  4476  iffalsed  4477  ifnefalse  4478  iftrueb  4479  ifsb  4480  ifbi  4489  ifeq1da  4498  ifeq12da  4500  ifclda  4502  ifeqda  4503  elimif  4504  ifbothda  4505  ifid  4507  ifnot  4519  ifan  4520  ifor  4521  2if2  4522  ifcomnan  4523  elimhyp  4532  elimhyp2v  4533  elimhyp3v  4534  elimhyp4v  4535  elimdhyp  4537  keephyp2v  4539  keephyp3v  4540  dfopif  4813  opprc  4839  somin1  6096  elimdelov  7463  brif1  7464  ovif12  7467  ifmpt2v  7469  oevn0  8450  pw2f1olem  9019  unxpdomlem2  9167  unxpdomlem3  9168  infsupprpr  9419  oi0  9443  wemaplem2  9462  ixpiunwdom  9505  cantnfp1lem3  9601  cantnflem1  9610  dfac12lem2  10067  fin23lem14  10255  axcc2lem  10358  ttukeylem5  10435  indval2  12164  uzin  12824  xrmax1  13127  xrmax2  13128  xrmin1  13129  xrmin2  13130  max1ALT  13138  ifle  13149  xmulneg1  13221  modifeq2int  13895  seqf1olem1  14003  seqf1olem2  14004  bcval3  14268  swrdccat  14697  pfxccat3a  14700  swrdccat3b  14702  repswswrd  14746  cshword  14753  ccatco  14797  sumrblem  15673  fsumcvg  15674  summolem2a  15677  sumss  15686  fsumcvg2  15689  sumsplit  15730  prodeq2ii  15876  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  zprod  15902  prodss  15912  ruclem2  16199  ruclem3  16200  flodddiv4  16384  sadadd2lem2  16419  sadcp1  16424  sadcaddlem  16426  gcdn0val  16467  dfgcd2  16515  lcmn0val  16564  lcmfn0val  16592  pcgcd  16849  pcmptcl  16862  pcmpt  16863  pcmpt2  16864  pcprod  16866  fldivp1  16868  prmreclem2  16888  prmreclem4  16890  vdwlem6  16957  prmop1  17009  fvprmselelfz  17015  fvprmselgcd1  17016  ressval2  17205  xpsaddlem  17537  xpsvsca  17541  mreexexd  17614  setcepi  18055  pmtrmvd  19431  fincygsubgodd  20089  obselocv  21708  mvrf1  21964  mplcoe3  22016  mplmon2  22039  psrbagsn  22041  evlslem1  22060  mhpsclcl  22113  mhpvarcl  22114  dmatmul  22462  1mavmul  22513  mulmarep1gsum2  22539  1marepvmarrepid  22540  mdetdiag  22564  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  mdetunilem7  22583  mdetunilem8  22584  mdetunilem9  22585  mndifsplit  22601  maducoeval2  22605  madugsum  22608  madurid  22609  smadiadetglem2  22637  1elcpmat  22680  decpmatid  22735  ptpjpre1  23536  ptbasfi  23546  isfcls  23974  ptcmplem2  24018  ptcmplem3  24019  dscmet  24537  dscopn  24538  icccmplem2  24789  cnmpopc  24895  iccpnfcnv  24911  xrhmeo  24913  pcoval2  24983  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  i1f1lem  25656  itg1addlem2  25664  itg1addlem3  25665  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  itg2const2  25708  itg2seq  25709  itg2uba  25710  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  iblss  25772  iblss2  25773  itgle  25777  itgss  25779  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  bddmulibl  25806  bddiblnc  25809  ditgneg  25824  elply2  26161  coeeq2  26207  dgrle  26208  coe1termlem  26223  logcnlem3  26608  igamgam  27012  isppw  27077  isnsqf  27098  mule1  27111  sqff1o  27145  chtublem  27174  dchrelbasd  27202  bposlem1  27247  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgsneg  27284  lgsdilem  27287  lgsdir2  27293  lgsdir  27295  lgsdi  27297  lgsne0  27298  gausslemma2dlem1a  27328  2lgslem1c  27356  2lgs  27370  dchrvmasum2if  27460  ostth2lem4  27599  nosupno  27667  nosupdm  27668  nosupbday  27669  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  noinfno  27682  noinfdm  27683  noinffv  27685  maxs1  27733  maxs2  27734  mins1  27735  mins2  27736  abssnid  28235  abssge0  28237  axlowdimlem15  29025  elimifd  32613  elim2if  32614  ifeq3da  32616  ifnetrue  32617  imadifxp  32671  pmtridf1o  33155  resvval2  33391  xrge0iifcnv  34077  ddeval0  34379  eulerpartlemb  34512  plymulx0  34691  signsw0glem  34697  signswmnd  34701  dfrdg2  35975  dfrdg3  35976  unisnif  36105  dfrdg4  36133  bj-xpima1sn  37263  finxpreclem2  37706  finxpreclem5  37711  matunitlindflem1  37937  poimirlem15  37956  poimirlem23  37964  mbfposadd  37988  itg2addnclem  37992  itg2addnclem3  37994  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem1  37999  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirclem5  38033  areacirc  38034  heiborlem4  38135  ac6s6  38493  riotaclbgBAD  39400  cdleme27a  40813  cdleme31sn2  40835  dihvalc  41679  mapdhval2  42172  hdmap1val2  42246  brif2  42665  brif12  42666  fsuppind  43023  dffltz  43067  pw2f1ocnv  43465  aomclem5  43486  arearect  43643  areaquad  43644  safesnsupfidom1o  43844  safesnsupfilb  43845  upbdrech2  45741  lptioo2  46061  lptioo1  46062  limsupmnfuzlem  46154  limsupre3uzlem  46163  limsup10exlem  46200  coskpi2  46294  cosknegpi  46297  icccncfext  46315  cncfiooicclem1  46321  cncfiooiccre  46323  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  itgioocnicc  46405  iblcncfioo  46406  volico  46411  sublevolico  46412  voliooico  46420  voliccico  46427  dirkerper  46524  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem10  46545  fourierdlem32  46567  fourierdlem33  46568  fourierdlem37  46572  fourierdlem62  46596  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem93  46627  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem15  46677  etransclem19  46681  etransclem23  46685  etransclem24  46686  etransclem25  46687  ioorrnopnxrlem  46734  nnfoctbdjlem  46883  isomenndlem  46958  ovn0  46994  hsphoidmvle2  47013  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1le  47022  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  hspdifhsp  47044  hoidifhspdmvle  47048  hspmbllem1  47054  hspmbllem2  47055  hspmbl  47057  volico2  47069  ovolval4lem2  47078  ovolval5lem1  47080  afvnfundmuv  47587  ndfatafv2  47659  difmodm1lt  47813  prproropf1olem4  47966  suppmptcfin  48852  linc1  48901  discsubc  49539  oppfrcl3  49605  eloppf  49608  eloppf2  49609  ifnmfalse  50238