Theorem iffalse 4484

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111  {cab 2709  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4476

This theorem is referenced by:  iffalsei  4485  iffalsed  4486  ifnefalse  4487  iftrueb  4488  ifsb  4489  ifbi  4498  ifeq1da  4507  ifeq12da  4509  ifclda  4511  ifeqda  4512  elimif  4513  ifbothda  4514  ifid  4516  ifnot  4528  ifan  4529  ifor  4530  2if2  4531  ifcomnan  4532  elimhyp  4541  elimhyp2v  4542  elimhyp3v  4543  elimhyp4v  4544  elimdhyp  4546  keephyp2v  4548  keephyp3v  4549  dfopif  4822  opprc  4848  somin1  6080  elimdelov  7442  brif1  7443  ovif12  7446  ifmpt2v  7448  oevn0  8430  pw2f1olem  8994  unxpdomlem2  9141  unxpdomlem3  9142  infsupprpr  9390  oi0  9414  wemaplem2  9433  ixpiunwdom  9476  cantnfp1lem3  9570  cantnflem1  9579  dfac12lem2  10033  fin23lem14  10221  axcc2lem  10324  ttukeylem5  10401  uzin  12769  xrmax1  13071  xrmax2  13072  xrmin1  13073  xrmin2  13074  max1ALT  13082  ifle  13093  xmulneg1  13165  modifeq2int  13837  seqf1olem1  13945  seqf1olem2  13946  bcval3  14210  swrdccat  14639  pfxccat3a  14642  swrdccat3b  14644  repswswrd  14688  cshword  14695  ccatco  14739  sumrblem  15615  fsumcvg  15616  summolem2a  15619  sumss  15628  fsumcvg2  15631  sumsplit  15672  prodeq2ii  15815  prodrblem  15833  fprodcvg  15834  prodmolem2a  15838  zprod  15841  prodss  15851  ruclem2  16138  ruclem3  16139  flodddiv4  16323  sadadd2lem2  16358  sadcp1  16363  sadcaddlem  16365  gcdn0val  16406  dfgcd2  16454  lcmn0val  16503  lcmfn0val  16531  pcgcd  16787  pcmptcl  16800  pcmpt  16801  pcmpt2  16802  pcprod  16804  fldivp1  16806  prmreclem2  16826  prmreclem4  16828  vdwlem6  16895  prmop1  16947  fvprmselelfz  16953  fvprmselgcd1  16954  ressval2  17143  xpsaddlem  17474  xpsvsca  17478  mreexexd  17551  setcepi  17992  pmtrmvd  19366  fincygsubgodd  20024  obselocv  21663  mvrf1  21921  mplcoe3  21971  mplmon2  21994  psrbagsn  21996  evlslem1  22015  mhpsclcl  22060  mhpvarcl  22061  dmatmul  22410  1mavmul  22461  mulmarep1gsum2  22487  1marepvmarrepid  22488  mdetdiag  22512  mdetrsca2  22517  mdetrlin2  22520  mdetunilem5  22529  mdetunilem7  22531  mdetunilem8  22532  mdetunilem9  22533  mndifsplit  22549  maducoeval2  22553  madugsum  22556  madurid  22557  smadiadetglem2  22585  1elcpmat  22628  decpmatid  22683  ptpjpre1  23484  ptbasfi  23494  isfcls  23922  ptcmplem2  23966  ptcmplem3  23967  dscmet  24485  dscopn  24486  icccmplem2  24737  cnmpopc  24847  iccpnfcnv  24867  xrhmeo  24869  pcoval2  24941  pcopt  24947  pcopt2  24948  pcoass  24949  pcorevlem  24951  i1f1lem  25615  itg1addlem2  25623  itg1addlem3  25624  i1fres  25631  itg1climres  25640  mbfi1fseqlem4  25644  mbfi1fseqlem5  25645  itg2const2  25667  itg2seq  25668  itg2uba  25669  itg2splitlem  25674  itg2split  25675  itg2monolem1  25676  itg2gt0  25686  itg2cnlem1  25687  itg2cnlem2  25688  iblss  25731  iblss2  25732  itgle  25736  itgss  25738  ibladdlem  25746  itgaddlem1  25749  iblabslem  25754  iblabs  25755  iblabsr  25756  iblmulc2  25757  bddmulibl  25765  bddiblnc  25768  ditgneg  25783  elply2  26126  coeeq2  26172  dgrle  26173  coe1termlem  26188  logcnlem3  26578  igamgam  26984  isppw  27049  isnsqf  27070  mule1  27083  sqff1o  27117  chtublem  27147  dchrelbasd  27175  bposlem1  27220  bposlem3  27222  bposlem5  27224  bposlem6  27225  lgsneg  27257  lgsdilem  27260  lgsdir2  27266  lgsdir  27268  lgsdi  27270  lgsne0  27271  gausslemma2dlem1a  27301  2lgslem1c  27329  2lgs  27343  dchrvmasum2if  27433  ostth2lem4  27572  nosupno  27640  nosupdm  27641  nosupbday  27642  nosupfv  27643  nosupres  27644  nosupbnd1lem1  27645  noinfno  27655  noinfdm  27656  noinffv  27658  maxs1  27702  maxs2  27703  mins1  27704  mins2  27705  abssnid  28179  abssge0  28181  axlowdimlem15  28932  elimifd  32518  elim2if  32519  ifeq3da  32521  ifnetrue  32522  imadifxp  32576  indval2  32830  pmtridf1o  33058  resvval2  33291  xrge0iifcnv  33941  ddeval0  34243  eulerpartlemb  34376  plymulx0  34555  signsw0glem  34561  signswmnd  34565  dfrdg2  35828  dfrdg3  35829  unisnif  35958  dfrdg4  35984  bj-xpima1sn  36989  finxpreclem2  37423  finxpreclem5  37428  matunitlindflem1  37655  poimirlem15  37674  poimirlem23  37682  mbfposadd  37706  itg2addnclem  37710  itg2addnclem3  37712  itg2gt0cn  37714  ibladdnclem  37715  itgaddnclem1  37717  iblabsnclem  37722  iblabsnc  37723  iblmulc2nc  37724  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  areacirclem5  37751  areacirc  37752  heiborlem4  37853  ac6s6  38211  riotaclbgBAD  38992  cdleme27a  40405  cdleme31sn2  40427  dihvalc  41271  mapdhval2  41764  hdmap1val2  41838  brif2  42256  brif12  42257  fsuppind  42622  dffltz  42666  pw2f1ocnv  43069  aomclem5  43090  arearect  43247  areaquad  43248  safesnsupfidom1o  43449  safesnsupfilb  43450  upbdrech2  45348  lptioo2  45670  lptioo1  45671  limsupmnfuzlem  45763  limsupre3uzlem  45772  limsup10exlem  45809  coskpi2  45903  cosknegpi  45906  icccncfext  45924  cncfiooicclem1  45930  cncfiooiccre  45932  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  itgioocnicc  46014  iblcncfioo  46015  volico  46020  sublevolico  46021  voliooico  46029  voliccico  46036  dirkerper  46133  dirkertrigeq  46138  dirkercncflem2  46141  fourierdlem10  46154  fourierdlem32  46176  fourierdlem33  46177  fourierdlem37  46181  fourierdlem62  46205  fourierdlem73  46216  fourierdlem74  46217  fourierdlem75  46218  fourierdlem79  46222  fourierdlem81  46224  fourierdlem82  46225  fourierdlem93  46236  fourierdlem97  46240  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  elaa2lem  46270  etransclem15  46286  etransclem19  46290  etransclem23  46294  etransclem24  46295  etransclem25  46296  ioorrnopnxrlem  46343  nnfoctbdjlem  46492  isomenndlem  46567  ovn0  46603  hsphoidmvle2  46622  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmv1le  46631  hoidmvlelem2  46633  hoidmvlelem3  46634  ovnhoilem1  46638  hspdifhsp  46653  hoidifhspdmvle  46657  hspmbllem1  46663  hspmbllem2  46664  hspmbl  46666  volico2  46678  ovolval4lem2  46687  ovolval5lem1  46689  afvnfundmuv  47169  ndfatafv2  47241  difmodm1lt  47389  prproropf1olem4  47536  suppmptcfin  48406  linc1  48456  discsubc  49095  oppfrcl3  49161  eloppf  49164  eloppf2  49165  ifnmfalse  49794