Theorem iffalse 4500

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cab 2708  ifcif 4491

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  iffalsei  4501  iffalsed  4502  ifnefalse  4503  iftrueb  4504  ifsb  4505  ifbi  4514  ifeq1da  4523  ifeq12da  4525  ifclda  4527  ifeqda  4528  elimif  4529  ifbothda  4530  ifid  4532  ifnot  4544  ifan  4545  ifor  4546  2if2  4547  ifcomnan  4548  elimhyp  4557  elimhyp2v  4558  elimhyp3v  4559  elimhyp4v  4560  elimdhyp  4562  keephyp2v  4564  keephyp3v  4565  dfopif  4837  opprc  4863  somin1  6109  elimdelov  7488  brif1  7489  ovif12  7492  ifmpt2v  7494  oevn0  8482  pw2f1olem  9050  unxpdomlem2  9205  unxpdomlem3  9206  infsupprpr  9464  oi0  9488  wemaplem2  9507  ixpiunwdom  9550  cantnfp1lem3  9640  cantnflem1  9649  dfac12lem2  10105  fin23lem14  10293  axcc2lem  10396  ttukeylem5  10473  uzin  12840  xrmax1  13142  xrmax2  13143  xrmin1  13144  xrmin2  13145  max1ALT  13153  ifle  13164  xmulneg1  13236  modifeq2int  13905  seqf1olem1  14013  seqf1olem2  14014  bcval3  14278  swrdccat  14707  pfxccat3a  14710  swrdccat3b  14712  repswswrd  14756  cshword  14763  ccatco  14808  sumrblem  15684  fsumcvg  15685  summolem2a  15688  sumss  15697  fsumcvg2  15700  sumsplit  15741  prodeq2ii  15884  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  zprod  15910  prodss  15920  ruclem2  16207  ruclem3  16208  flodddiv4  16392  sadadd2lem2  16427  sadcp1  16432  sadcaddlem  16434  gcdn0val  16475  dfgcd2  16523  lcmn0val  16572  lcmfn0val  16600  pcgcd  16856  pcmptcl  16869  pcmpt  16870  pcmpt2  16871  pcprod  16873  fldivp1  16875  prmreclem2  16895  prmreclem4  16897  vdwlem6  16964  prmop1  17016  fvprmselelfz  17022  fvprmselgcd1  17023  ressval2  17212  xpsaddlem  17543  xpsvsca  17547  mreexexd  17616  setcepi  18057  pmtrmvd  19393  fincygsubgodd  20051  obselocv  21644  mvrf1  21902  mplcoe3  21952  mplmon2  21975  psrbagsn  21977  evlslem1  21996  mhpsclcl  22041  mhpvarcl  22042  dmatmul  22391  1mavmul  22442  mulmarep1gsum2  22468  1marepvmarrepid  22469  mdetdiag  22493  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  mdetunilem7  22512  mdetunilem8  22513  mdetunilem9  22514  mndifsplit  22530  maducoeval2  22534  madugsum  22537  madurid  22538  smadiadetglem2  22566  1elcpmat  22609  decpmatid  22664  ptpjpre1  23465  ptbasfi  23475  isfcls  23903  ptcmplem2  23947  ptcmplem3  23948  dscmet  24467  dscopn  24468  icccmplem2  24719  cnmpopc  24829  iccpnfcnv  24849  xrhmeo  24851  pcoval2  24923  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  i1f1lem  25597  itg1addlem2  25605  itg1addlem3  25606  i1fres  25613  itg1climres  25622  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  itg2const2  25649  itg2seq  25650  itg2uba  25651  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  iblss2  25714  itgle  25718  itgss  25720  ibladdlem  25728  itgaddlem1  25731  iblabslem  25736  iblabs  25737  iblabsr  25738  iblmulc2  25739  bddmulibl  25747  bddiblnc  25750  ditgneg  25765  elply2  26108  coeeq2  26154  dgrle  26155  coe1termlem  26170  logcnlem3  26560  igamgam  26966  isppw  27031  isnsqf  27052  mule1  27065  sqff1o  27099  chtublem  27129  dchrelbasd  27157  bposlem1  27202  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgsneg  27239  lgsdilem  27242  lgsdir2  27248  lgsdir  27250  lgsdi  27252  lgsne0  27253  gausslemma2dlem1a  27283  2lgslem1c  27311  2lgs  27325  dchrvmasum2if  27415  ostth2lem4  27554  nosupno  27622  nosupdm  27623  nosupbday  27624  nosupfv  27625  nosupres  27626  nosupbnd1lem1  27627  noinfno  27637  noinfdm  27638  noinffv  27640  maxs1  27684  maxs2  27685  mins1  27686  mins2  27687  abssnid  28152  abssge0  28154  axlowdimlem15  28890  elimifd  32479  elim2if  32480  ifeq3da  32482  ifnetrue  32483  imadifxp  32537  indval2  32784  pmtridf1o  33058  resvval2  33310  xrge0iifcnv  33930  ddeval0  34232  eulerpartlemb  34366  plymulx0  34545  signsw0glem  34551  signswmnd  34555  dfrdg2  35790  dfrdg3  35791  unisnif  35920  dfrdg4  35946  bj-xpima1sn  36951  finxpreclem2  37385  finxpreclem5  37390  matunitlindflem1  37617  poimirlem15  37636  poimirlem23  37644  mbfposadd  37668  itg2addnclem  37672  itg2addnclem3  37674  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem1  37679  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  areacirclem5  37713  areacirc  37714  heiborlem4  37815  ac6s6  38173  riotaclbgBAD  38954  cdleme27a  40368  cdleme31sn2  40390  dihvalc  41234  mapdhval2  41727  hdmap1val2  41801  brif2  42219  brif12  42220  fsuppind  42585  dffltz  42629  pw2f1ocnv  43033  aomclem5  43054  arearect  43211  areaquad  43212  safesnsupfidom1o  43413  safesnsupfilb  43414  upbdrech2  45313  lptioo2  45636  lptioo1  45637  limsupmnfuzlem  45731  limsupre3uzlem  45740  limsup10exlem  45777  coskpi2  45871  cosknegpi  45874  icccncfext  45892  cncfiooicclem1  45898  cncfiooiccre  45900  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  itgioocnicc  45982  iblcncfioo  45983  volico  45988  sublevolico  45989  voliooico  45997  voliccico  46004  dirkerper  46101  dirkertrigeq  46106  dirkercncflem2  46109  fourierdlem10  46122  fourierdlem32  46144  fourierdlem33  46145  fourierdlem37  46149  fourierdlem62  46173  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem93  46204  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  etransclem15  46254  etransclem19  46258  etransclem23  46262  etransclem24  46263  etransclem25  46264  ioorrnopnxrlem  46311  nnfoctbdjlem  46460  isomenndlem  46535  ovn0  46571  hsphoidmvle2  46590  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  hspdifhsp  46621  hoidifhspdmvle  46625  hspmbllem1  46631  hspmbllem2  46632  hspmbl  46634  volico2  46646  ovolval4lem2  46655  ovolval5lem1  46657  afvnfundmuv  47144  ndfatafv2  47216  difmodm1lt  47364  prproropf1olem4  47511  suppmptcfin  48368  linc1  48418  discsubc  49057  oppfrcl3  49123  eloppf  49126  eloppf2  49127  ifnmfalse  49756