Theorem iffalse 4487

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 4479	. 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 4478

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 4479

This theorem is referenced by:  iffalsei  4488  iffalsed  4489  ifnefalse  4490  iftrueb  4491  ifsb  4492  ifbi  4501  ifeq1da  4510  ifeq12da  4512  ifclda  4514  ifeqda  4515  elimif  4516  ifbothda  4517  ifid  4519  ifnot  4531  ifan  4532  ifor  4533  2if2  4534  ifcomnan  4535  elimhyp  4544  elimhyp2v  4545  elimhyp3v  4546  elimhyp4v  4547  elimdhyp  4549  keephyp2v  4551  keephyp3v  4552  dfopif  4824  opprc  4850  somin1  6086  elimdelov  7449  brif1  7450  ovif12  7453  ifmpt2v  7455  oevn0  8440  pw2f1olem  9005  unxpdomlem2  9156  unxpdomlem3  9157  infsupprpr  9415  oi0  9439  wemaplem2  9458  ixpiunwdom  9501  cantnfp1lem3  9595  cantnflem1  9604  dfac12lem2  10058  fin23lem14  10246  axcc2lem  10349  ttukeylem5  10426  uzin  12793  xrmax1  13095  xrmax2  13096  xrmin1  13097  xrmin2  13098  max1ALT  13106  ifle  13117  xmulneg1  13189  modifeq2int  13858  seqf1olem1  13966  seqf1olem2  13967  bcval3  14231  swrdccat  14659  pfxccat3a  14662  swrdccat3b  14664  repswswrd  14708  cshword  14715  ccatco  14760  sumrblem  15636  fsumcvg  15637  summolem2a  15640  sumss  15649  fsumcvg2  15652  sumsplit  15693  prodeq2ii  15836  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  zprod  15862  prodss  15872  ruclem2  16159  ruclem3  16160  flodddiv4  16344  sadadd2lem2  16379  sadcp1  16384  sadcaddlem  16386  gcdn0val  16427  dfgcd2  16475  lcmn0val  16524  lcmfn0val  16552  pcgcd  16808  pcmptcl  16821  pcmpt  16822  pcmpt2  16823  pcprod  16825  fldivp1  16827  prmreclem2  16847  prmreclem4  16849  vdwlem6  16916  prmop1  16968  fvprmselelfz  16974  fvprmselgcd1  16975  ressval2  17164  xpsaddlem  17495  xpsvsca  17499  mreexexd  17572  setcepi  18013  pmtrmvd  19353  fincygsubgodd  20011  obselocv  21653  mvrf1  21911  mplcoe3  21961  mplmon2  21984  psrbagsn  21986  evlslem1  22005  mhpsclcl  22050  mhpvarcl  22051  dmatmul  22400  1mavmul  22451  mulmarep1gsum2  22477  1marepvmarrepid  22478  mdetdiag  22502  mdetrsca2  22507  mdetrlin2  22510  mdetunilem5  22519  mdetunilem7  22521  mdetunilem8  22522  mdetunilem9  22523  mndifsplit  22539  maducoeval2  22543  madugsum  22546  madurid  22547  smadiadetglem2  22575  1elcpmat  22618  decpmatid  22673  ptpjpre1  23474  ptbasfi  23484  isfcls  23912  ptcmplem2  23956  ptcmplem3  23957  dscmet  24476  dscopn  24477  icccmplem2  24728  cnmpopc  24838  iccpnfcnv  24858  xrhmeo  24860  pcoval2  24932  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevlem  24942  i1f1lem  25606  itg1addlem2  25614  itg1addlem3  25615  i1fres  25622  itg1climres  25631  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  itg2const2  25658  itg2seq  25659  itg2uba  25660  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25722  iblss2  25723  itgle  25727  itgss  25729  ibladdlem  25737  itgaddlem1  25740  iblabslem  25745  iblabs  25746  iblabsr  25747  iblmulc2  25748  bddmulibl  25756  bddiblnc  25759  ditgneg  25774  elply2  26117  coeeq2  26163  dgrle  26164  coe1termlem  26179  logcnlem3  26569  igamgam  26975  isppw  27040  isnsqf  27061  mule1  27074  sqff1o  27108  chtublem  27138  dchrelbasd  27166  bposlem1  27211  bposlem3  27213  bposlem5  27215  bposlem6  27216  lgsneg  27248  lgsdilem  27251  lgsdir2  27257  lgsdir  27259  lgsdi  27261  lgsne0  27262  gausslemma2dlem1a  27292  2lgslem1c  27320  2lgs  27334  dchrvmasum2if  27424  ostth2lem4  27563  nosupno  27631  nosupdm  27632  nosupbday  27633  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  noinfno  27646  noinfdm  27647  noinffv  27649  maxs1  27693  maxs2  27694  mins1  27695  mins2  27696  abssnid  28168  abssge0  28170  axlowdimlem15  28919  elimifd  32505  elim2if  32506  ifeq3da  32508  ifnetrue  32509  imadifxp  32563  indval2  32810  pmtridf1o  33049  resvval2  33279  xrge0iifcnv  33899  ddeval0  34201  eulerpartlemb  34335  plymulx0  34514  signsw0glem  34520  signswmnd  34524  dfrdg2  35768  dfrdg3  35769  unisnif  35898  dfrdg4  35924  bj-xpima1sn  36929  finxpreclem2  37363  finxpreclem5  37368  matunitlindflem1  37595  poimirlem15  37614  poimirlem23  37622  mbfposadd  37646  itg2addnclem  37650  itg2addnclem3  37652  itg2gt0cn  37654  ibladdnclem  37655  itgaddnclem1  37657  iblabsnclem  37662  iblabsnc  37663  iblmulc2nc  37664  ftc1anclem5  37676  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  areacirclem5  37691  areacirc  37692  heiborlem4  37793  ac6s6  38151  riotaclbgBAD  38932  cdleme27a  40346  cdleme31sn2  40368  dihvalc  41212  mapdhval2  41705  hdmap1val2  41779  brif2  42197  brif12  42198  fsuppind  42563  dffltz  42607  pw2f1ocnv  43010  aomclem5  43031  arearect  43188  areaquad  43189  safesnsupfidom1o  43390  safesnsupfilb  43391  upbdrech2  45290  lptioo2  45613  lptioo1  45614  limsupmnfuzlem  45708  limsupre3uzlem  45717  limsup10exlem  45754  coskpi2  45848  cosknegpi  45851  icccncfext  45869  cncfiooicclem1  45875  cncfiooiccre  45877  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  itgioocnicc  45959  iblcncfioo  45960  volico  45965  sublevolico  45966  voliooico  45974  voliccico  45981  dirkerper  46078  dirkertrigeq  46083  dirkercncflem2  46086  fourierdlem10  46099  fourierdlem32  46121  fourierdlem33  46122  fourierdlem37  46126  fourierdlem62  46150  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem79  46167  fourierdlem81  46169  fourierdlem82  46170  fourierdlem93  46181  fourierdlem97  46185  fourierdlem101  46189  fourierdlem103  46191  fourierdlem104  46192  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  elaa2lem  46215  etransclem15  46231  etransclem19  46235  etransclem23  46239  etransclem24  46240  etransclem25  46241  ioorrnopnxrlem  46288  nnfoctbdjlem  46437  isomenndlem  46512  ovn0  46548  hsphoidmvle2  46567  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmv1le  46576  hoidmvlelem2  46578  hoidmvlelem3  46579  ovnhoilem1  46583  hspdifhsp  46598  hoidifhspdmvle  46602  hspmbllem1  46608  hspmbllem2  46609  hspmbl  46611  volico2  46623  ovolval4lem2  46632  ovolval5lem1  46634  afvnfundmuv  47124  ndfatafv2  47196  difmodm1lt  47344  prproropf1olem4  47491  suppmptcfin  48361  linc1  48411  discsubc  49050  oppfrcl3  49116  eloppf  49119  eloppf2  49120  ifnmfalse  49749