Theorem iffalse 4497

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  iffalsei  4498  iffalsed  4499  ifnefalse  4500  iftrueb  4501  ifsb  4502  ifbi  4511  ifeq1da  4520  ifeq12da  4522  ifclda  4524  ifeqda  4525  elimif  4526  ifbothda  4527  ifid  4529  ifnot  4541  ifan  4542  ifor  4543  2if2  4544  ifcomnan  4545  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elimdhyp  4559  keephyp2v  4561  keephyp3v  4562  dfopif  4834  opprc  4860  somin1  6106  elimdelov  7485  brif1  7486  ovif12  7489  ifmpt2v  7491  oevn0  8479  pw2f1olem  9045  unxpdomlem2  9198  unxpdomlem3  9199  infsupprpr  9457  oi0  9481  wemaplem2  9500  ixpiunwdom  9543  cantnfp1lem3  9633  cantnflem1  9642  dfac12lem2  10098  fin23lem14  10286  axcc2lem  10389  ttukeylem5  10466  uzin  12833  xrmax1  13135  xrmax2  13136  xrmin1  13137  xrmin2  13138  max1ALT  13146  ifle  13157  xmulneg1  13229  modifeq2int  13898  seqf1olem1  14006  seqf1olem2  14007  bcval3  14271  swrdccat  14700  pfxccat3a  14703  swrdccat3b  14705  repswswrd  14749  cshword  14756  ccatco  14801  sumrblem  15677  fsumcvg  15678  summolem2a  15681  sumss  15690  fsumcvg2  15693  sumsplit  15734  prodeq2ii  15877  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  zprod  15903  prodss  15913  ruclem2  16200  ruclem3  16201  flodddiv4  16385  sadadd2lem2  16420  sadcp1  16425  sadcaddlem  16427  gcdn0val  16468  dfgcd2  16516  lcmn0val  16565  lcmfn0val  16593  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  17536  xpsvsca  17540  mreexexd  17609  setcepi  18050  pmtrmvd  19386  fincygsubgodd  20044  obselocv  21637  mvrf1  21895  mplcoe3  21945  mplmon2  21968  psrbagsn  21970  evlslem1  21989  mhpsclcl  22034  mhpvarcl  22035  dmatmul  22384  1mavmul  22435  mulmarep1gsum2  22461  1marepvmarrepid  22462  mdetdiag  22486  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  mdetunilem7  22505  mdetunilem8  22506  mdetunilem9  22507  mndifsplit  22523  maducoeval2  22527  madugsum  22530  madurid  22531  smadiadetglem2  22559  1elcpmat  22602  decpmatid  22657  ptpjpre1  23458  ptbasfi  23468  isfcls  23896  ptcmplem2  23940  ptcmplem3  23941  dscmet  24460  dscopn  24461  icccmplem2  24712  cnmpopc  24822  iccpnfcnv  24842  xrhmeo  24844  pcoval2  24916  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  i1f1lem  25590  itg1addlem2  25598  itg1addlem3  25599  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  itg2const2  25642  itg2seq  25643  itg2uba  25644  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  iblss2  25707  itgle  25711  itgss  25713  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  iblabs  25730  iblabsr  25731  iblmulc2  25732  bddmulibl  25740  bddiblnc  25743  ditgneg  25758  elply2  26101  coeeq2  26147  dgrle  26148  coe1termlem  26163  logcnlem3  26553  igamgam  26959  isppw  27024  isnsqf  27045  mule1  27058  sqff1o  27092  chtublem  27122  dchrelbasd  27150  bposlem1  27195  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgsneg  27232  lgsdilem  27235  lgsdir2  27241  lgsdir  27243  lgsdi  27245  lgsne0  27246  gausslemma2dlem1a  27276  2lgslem1c  27304  2lgs  27318  dchrvmasum2if  27408  ostth2lem4  27547  nosupno  27615  nosupdm  27616  nosupbday  27617  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  noinfno  27630  noinfdm  27631  noinffv  27633  maxs1  27677  maxs2  27678  mins1  27679  mins2  27680  abssnid  28145  abssge0  28147  axlowdimlem15  28883  elimifd  32472  elim2if  32473  ifeq3da  32475  ifnetrue  32476  imadifxp  32530  indval2  32777  pmtridf1o  33051  resvval2  33303  xrge0iifcnv  33923  ddeval0  34225  eulerpartlemb  34359  plymulx0  34538  signsw0glem  34544  signswmnd  34548  dfrdg2  35783  dfrdg3  35784  unisnif  35913  dfrdg4  35939  bj-xpima1sn  36944  finxpreclem2  37378  finxpreclem5  37383  matunitlindflem1  37610  poimirlem15  37629  poimirlem23  37637  mbfposadd  37661  itg2addnclem  37665  itg2addnclem3  37667  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem1  37672  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem5  37706  areacirc  37707  heiborlem4  37808  ac6s6  38166  riotaclbgBAD  38947  cdleme27a  40361  cdleme31sn2  40383  dihvalc  41227  mapdhval2  41720  hdmap1val2  41794  brif2  42212  brif12  42213  fsuppind  42578  dffltz  42622  pw2f1ocnv  43026  aomclem5  43047  arearect  43204  areaquad  43205  safesnsupfidom1o  43406  safesnsupfilb  43407  upbdrech2  45306  lptioo2  45629  lptioo1  45630  limsupmnfuzlem  45724  limsupre3uzlem  45733  limsup10exlem  45770  coskpi2  45864  cosknegpi  45867  icccncfext  45885  cncfiooicclem1  45891  cncfiooiccre  45893  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  itgioocnicc  45975  iblcncfioo  45976  volico  45981  sublevolico  45982  voliooico  45990  voliccico  45997  dirkerper  46094  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem10  46115  fourierdlem32  46137  fourierdlem33  46138  fourierdlem37  46142  fourierdlem62  46166  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem93  46197  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem15  46247  etransclem19  46251  etransclem23  46255  etransclem24  46256  etransclem25  46257  ioorrnopnxrlem  46304  nnfoctbdjlem  46453  isomenndlem  46528  ovn0  46564  hsphoidmvle2  46583  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  hspdifhsp  46614  hoidifhspdmvle  46618  hspmbllem1  46624  hspmbllem2  46625  hspmbl  46627  volico2  46639  ovolval4lem2  46648  ovolval5lem1  46650  afvnfundmuv  47140  ndfatafv2  47212  difmodm1lt  47360  prproropf1olem4  47507  suppmptcfin  48364  linc1  48414  discsubc  49053  oppfrcl3  49119  eloppf  49122  eloppf2  49123  ifnmfalse  49752