Theorem iffalse 4509

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108  {cab 2713  ifcif 4500

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  iffalsei  4510  iffalsed  4511  ifnefalse  4512  iftrueb  4513  ifsb  4514  ifbi  4523  ifeq1da  4532  ifeq12da  4534  ifclda  4536  ifeqda  4537  elimif  4538  ifbothda  4539  ifid  4541  ifnot  4553  ifan  4554  ifor  4555  2if2  4556  ifcomnan  4557  elimhyp  4566  elimhyp2v  4567  elimhyp3v  4568  elimhyp4v  4569  elimdhyp  4571  keephyp2v  4573  keephyp3v  4574  dfopif  4846  opprc  4872  somin1  6122  elimdelov  7503  brif1  7504  ovif12  7507  ifmpt2v  7509  oevn0  8527  pw2f1olem  9090  unxpdomlem2  9259  unxpdomlem3  9260  infsupprpr  9518  oi0  9542  wemaplem2  9561  ixpiunwdom  9604  cantnfp1lem3  9694  cantnflem1  9703  dfac12lem2  10159  fin23lem14  10347  axcc2lem  10450  ttukeylem5  10527  uzin  12892  xrmax1  13191  xrmax2  13192  xrmin1  13193  xrmin2  13194  max1ALT  13202  ifle  13213  xmulneg1  13285  modifeq2int  13951  seqf1olem1  14059  seqf1olem2  14060  bcval3  14324  swrdccat  14753  pfxccat3a  14756  swrdccat3b  14758  repswswrd  14802  cshword  14809  ccatco  14854  sumrblem  15727  fsumcvg  15728  summolem2a  15731  sumss  15740  fsumcvg2  15743  sumsplit  15784  prodeq2ii  15927  prodrblem  15945  fprodcvg  15946  prodmolem2a  15950  zprod  15953  prodss  15963  ruclem2  16250  ruclem3  16251  flodddiv4  16434  sadadd2lem2  16469  sadcp1  16474  sadcaddlem  16476  gcdn0val  16517  dfgcd2  16565  lcmn0val  16614  lcmfn0val  16642  pcgcd  16898  pcmptcl  16911  pcmpt  16912  pcmpt2  16913  pcprod  16915  fldivp1  16917  prmreclem2  16937  prmreclem4  16939  vdwlem6  17006  prmop1  17058  fvprmselelfz  17064  fvprmselgcd1  17065  ressval2  17256  xpsaddlem  17587  xpsvsca  17591  mreexexd  17660  setcepi  18101  pmtrmvd  19437  fincygsubgodd  20095  obselocv  21688  mvrf1  21946  mplcoe3  21996  mplmon2  22019  psrbagsn  22021  evlslem1  22040  mhpsclcl  22085  mhpvarcl  22086  dmatmul  22435  1mavmul  22486  mulmarep1gsum2  22512  1marepvmarrepid  22513  mdetdiag  22537  mdetrsca2  22542  mdetrlin2  22545  mdetunilem5  22554  mdetunilem7  22556  mdetunilem8  22557  mdetunilem9  22558  mndifsplit  22574  maducoeval2  22578  madugsum  22581  madurid  22582  smadiadetglem2  22610  1elcpmat  22653  decpmatid  22708  ptpjpre1  23509  ptbasfi  23519  isfcls  23947  ptcmplem2  23991  ptcmplem3  23992  dscmet  24511  dscopn  24512  icccmplem2  24763  cnmpopc  24873  iccpnfcnv  24893  xrhmeo  24895  pcoval2  24967  pcopt  24973  pcopt2  24974  pcoass  24975  pcorevlem  24977  i1f1lem  25642  itg1addlem2  25650  itg1addlem3  25651  i1fres  25658  itg1climres  25667  mbfi1fseqlem4  25671  mbfi1fseqlem5  25672  itg2const2  25694  itg2seq  25695  itg2uba  25696  itg2splitlem  25701  itg2split  25702  itg2monolem1  25703  itg2gt0  25713  itg2cnlem1  25714  itg2cnlem2  25715  iblss  25758  iblss2  25759  itgle  25763  itgss  25765  ibladdlem  25773  itgaddlem1  25776  iblabslem  25781  iblabs  25782  iblabsr  25783  iblmulc2  25784  bddmulibl  25792  bddiblnc  25795  ditgneg  25810  elply2  26153  coeeq2  26199  dgrle  26200  coe1termlem  26215  logcnlem3  26605  igamgam  27011  isppw  27076  isnsqf  27097  mule1  27110  sqff1o  27144  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  27729  maxs2  27730  mins1  27731  mins2  27732  abssnid  28197  abssge0  28199  axlowdimlem15  28935  elimifd  32524  elim2if  32525  ifeq3da  32527  ifnetrue  32528  imadifxp  32582  indval2  32831  pmtridf1o  33105  resvval2  33347  xrge0iifcnv  33964  ddeval0  34266  eulerpartlemb  34400  plymulx0  34579  signsw0glem  34585  signswmnd  34589  dfrdg2  35813  dfrdg3  35814  unisnif  35943  dfrdg4  35969  bj-xpima1sn  36974  finxpreclem2  37408  finxpreclem5  37413  matunitlindflem1  37640  poimirlem15  37659  poimirlem23  37667  mbfposadd  37691  itg2addnclem  37695  itg2addnclem3  37697  itg2gt0cn  37699  ibladdnclem  37700  itgaddnclem1  37702  iblabsnclem  37707  iblabsnc  37708  iblmulc2nc  37709  ftc1anclem5  37721  ftc1anclem7  37723  ftc1anclem8  37724  ftc1anc  37725  areacirclem5  37736  areacirc  37737  heiborlem4  37838  ac6s6  38196  riotaclbgBAD  38972  cdleme27a  40386  cdleme31sn2  40408  dihvalc  41252  mapdhval2  41745  hdmap1val2  41819  metakunt6  42223  metakunt7  42224  metakunt8  42225  metakunt11  42228  metakunt12  42229  metakunt22  42239  brif2  42275  brif12  42276  fsuppind  42613  dffltz  42657  pw2f1ocnv  43061  aomclem5  43082  arearect  43239  areaquad  43240  safesnsupfidom1o  43441  safesnsupfilb  43442  upbdrech2  45337  lptioo2  45660  lptioo1  45661  limsupmnfuzlem  45755  limsupre3uzlem  45764  limsup10exlem  45801  coskpi2  45895  cosknegpi  45898  icccncfext  45916  cncfiooicclem1  45922  cncfiooiccre  45924  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  itgioocnicc  46006  iblcncfioo  46007  volico  46012  sublevolico  46013  voliooico  46021  voliccico  46028  dirkerper  46125  dirkertrigeq  46130  dirkercncflem2  46133  fourierdlem10  46146  fourierdlem32  46168  fourierdlem33  46169  fourierdlem37  46173  fourierdlem62  46197  fourierdlem73  46208  fourierdlem74  46209  fourierdlem75  46210  fourierdlem79  46214  fourierdlem81  46216  fourierdlem82  46217  fourierdlem93  46228  fourierdlem97  46232  fourierdlem101  46236  fourierdlem103  46238  fourierdlem104  46239  sqwvfoura  46257  sqwvfourb  46258  fourierswlem  46259  fouriersw  46260  elaa2lem  46262  etransclem15  46278  etransclem19  46282  etransclem23  46286  etransclem24  46287  etransclem25  46288  ioorrnopnxrlem  46335  nnfoctbdjlem  46484  isomenndlem  46559  ovn0  46595  hsphoidmvle2  46614  hoidmv1lelem1  46620  hoidmv1lelem2  46621  hoidmv1le  46623  hoidmvlelem2  46625  hoidmvlelem3  46626  ovnhoilem1  46630  hspdifhsp  46645  hoidifhspdmvle  46649  hspmbllem1  46655  hspmbllem2  46656  hspmbl  46658  volico2  46670  ovolval4lem2  46679  ovolval5lem1  46681  afvnfundmuv  47168  ndfatafv2  47240  prproropf1olem4  47520  suppmptcfin  48351  linc1  48401  discsubc  49031  oppfrcl3  49078  ifnmfalse  49627