Theorem iffalse 4470

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119  {cab 2718  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  iffalsei  4471  iffalsed  4472  ifnefalse  4473  iftrueb  4474  ifsb  4475  ifbi  4484  ifeq1da  4493  ifeq12da  4495  ifclda  4497  ifeqda  4498  elimif  4499  ifbothda  4500  ifid  4502  ifnot  4514  ifan  4515  ifor  4516  2if2  4517  ifcomnan  4518  elimhyp  4527  elimhyp2v  4528  elimhyp3v  4529  elimhyp4v  4530  elimdhyp  4532  keephyp2v  4534  keephyp3v  4535  dfopif  4808  opprc  4834  somin1  6090  elimdelov  7459  brif1  7460  ovif12  7463  ifmpt2v  7465  oevn0  8447  pw2f1olem  9016  unxpdomlem2  9164  unxpdomlem3  9165  infsupprpr  9416  oi0  9440  wemaplem2  9459  ixpiunwdom  9502  cantnfp1lem3  9599  cantnflem1  9608  dfac12lem2  10065  fin23lem14  10253  axcc2lem  10356  ttukeylem5  10433  indval2  12162  uzin  12822  xrmax1  13125  xrmax2  13126  xrmin1  13127  xrmin2  13128  max1ALT  13136  ifle  13147  xmulneg1  13219  modifeq2int  13893  seqf1olem1  14001  seqf1olem2  14002  bcval3  14266  swrdccat  14695  pfxccat3a  14698  swrdccat3b  14700  repswswrd  14744  cshword  14751  ccatco  14795  sumrblem  15671  fsumcvg  15672  summolem2a  15675  sumss  15684  fsumcvg2  15687  sumsplit  15728  prodeq2ii  15874  prodrblem  15892  fprodcvg  15893  prodmolem2a  15897  zprod  15900  prodss  15910  ruclem2  16197  ruclem3  16198  flodddiv4  16382  sadadd2lem2  16417  sadcp1  16422  sadcaddlem  16424  gcdn0val  16465  dfgcd2  16513  lcmn0val  16562  lcmfn0val  16590  pcgcd  16847  pcmptcl  16860  pcmpt  16861  pcmpt2  16862  pcprod  16864  fldivp1  16866  prmreclem2  16886  prmreclem4  16888  vdwlem6  16955  prmop1  17007  fvprmselelfz  17013  fvprmselgcd1  17014  ressval2  17203  xpsaddlem  17535  xpsvsca  17539  mreexexd  17612  setcepi  18053  pmtrmvd  19429  fincygsubgodd  20087  obselocv  21710  mvrf1  21967  mplcoe3  22021  mplmon2  22044  psrbagsn  22046  evlslem1  22065  mhpsclcl  22142  mhpvarcl  22143  dmatmul  22487  1mavmul  22538  mulmarep1gsum2  22564  1marepvmarrepid  22565  mdetdiag  22589  mdetrsca2  22594  mdetrlin2  22597  mdetunilem5  22606  mdetunilem7  22608  mdetunilem8  22609  mdetunilem9  22610  mndifsplit  22626  maducoeval2  22630  madugsum  22633  madurid  22634  smadiadetglem2  22662  1elcpmat  22705  decpmatid  22760  ptpjpre1  23561  ptbasfi  23571  isfcls  23999  ptcmplem2  24043  ptcmplem3  24044  dscmet  24562  dscopn  24563  icccmplem2  24814  cnmpopc  24920  iccpnfcnv  24936  xrhmeo  24938  pcoval2  25008  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  i1f1lem  25681  itg1addlem2  25689  itg1addlem3  25690  i1fres  25697  itg1climres  25706  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  itg2const2  25733  itg2seq  25734  itg2uba  25735  itg2splitlem  25740  itg2split  25741  itg2monolem1  25742  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  iblss  25797  iblss2  25798  itgle  25802  itgss  25804  ibladdlem  25812  itgaddlem1  25815  iblabslem  25820  iblabs  25821  iblabsr  25822  iblmulc2  25823  bddmulibl  25831  bddiblnc  25834  ditgneg  25849  elply2  26186  coeeq2  26232  dgrle  26233  coe1termlem  26248  logcnlem3  26633  igamgam  27037  isppw  27102  isnsqf  27123  mule1  27136  sqff1o  27170  chtublem  27199  dchrelbasd  27227  bposlem1  27272  bposlem3  27274  bposlem5  27276  bposlem6  27277  lgsneg  27309  lgsdilem  27312  lgsdir2  27318  lgsdir  27320  lgsdi  27322  lgsne0  27323  gausslemma2dlem1a  27353  2lgslem1c  27381  2lgs  27395  dchrvmasum2if  27485  ostth2lem4  27624  nosupno  27692  nosupdm  27693  nosupbday  27694  nosupfv  27695  nosupres  27696  nosupbnd1lem1  27697  noinfno  27707  noinfdm  27708  noinffv  27710  maxs1  27758  maxs2  27759  mins1  27760  mins2  27761  abssnid  28260  abssge0  28262  axlowdimlem15  29050  elimifd  32638  elim2if  32639  ifeq3da  32641  ifnetrue  32642  imadifxp  32697  pmtridf1o  33182  resvval2  33421  xrge0iifcnv  34124  ddeval0  34426  eulerpartlemb  34559  plymulx0  34738  signsw0glem  34744  signswmnd  34748  dfrdg2  36028  dfrdg3  36029  unisnif  36158  dfrdg4  36186  bj-xpima1sn  37316  finxpreclem2  37759  finxpreclem5  37764  matunitlindflem1  37990  poimirlem15  38009  poimirlem23  38017  mbfposadd  38041  itg2addnclem  38045  itg2addnclem3  38047  itg2gt0cn  38049  ibladdnclem  38050  itgaddnclem1  38052  iblabsnclem  38057  iblabsnc  38058  iblmulc2nc  38059  ftc1anclem5  38071  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  areacirclem5  38086  areacirc  38087  heiborlem4  38188  ac6s6  38546  riotaclbgBAD  39453  cdleme27a  40866  cdleme31sn2  40888  dihvalc  41732  mapdhval2  42225  hdmap1val2  42299  brif2  42718  brif12  42719  fsuppind  43047  dffltz  43091  pw2f1ocnv  43489  aomclem5  43510  arearect  43667  areaquad  43668  safesnsupfidom1o  43868  safesnsupfilb  43869  upbdrech2  45763  lptioo2  46083  lptioo1  46084  limsupmnfuzlem  46176  limsupre3uzlem  46185  limsup10exlem  46222  coskpi2  46316  cosknegpi  46319  icccncfext  46337  cncfiooicclem1  46343  cncfiooiccre  46345  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  itgioocnicc  46427  iblcncfioo  46428  volico  46433  sublevolico  46434  voliooico  46442  voliccico  46449  dirkerper  46546  dirkertrigeq  46551  dirkercncflem2  46554  fourierdlem10  46567  fourierdlem32  46589  fourierdlem33  46590  fourierdlem37  46594  fourierdlem62  46618  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem79  46635  fourierdlem81  46637  fourierdlem82  46638  fourierdlem93  46649  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  elaa2lem  46683  etransclem15  46699  etransclem19  46703  etransclem23  46707  etransclem24  46708  etransclem25  46709  ioorrnopnxrlem  46756  nnfoctbdjlem  46905  isomenndlem  46980  ovn0  47016  hsphoidmvle2  47035  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1le  47044  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem1  47051  hspdifhsp  47066  hoidifhspdmvle  47070  hspmbllem1  47076  hspmbllem2  47077  hspmbl  47079  volico2  47091  ovolval4lem2  47100  ovolval5lem1  47102  afvnfundmuv  47609  ndfatafv2  47681  difmodm1lt  47835  prproropf1olem4  47988  suppmptcfin  48874  linc1  48923  discsubc  49561  oppfrcl3  49627  eloppf  49630  eloppf2  49631  ifnmfalse  50260