Theorem iffalse 4475

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		dedlemb 1041	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
2	1	abbi2dv 2950	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
3		df-if 4467	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
4	2, 3	syl6reqr 2875	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1533   ∈ wcel 2110  {cab 2799  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4467

This theorem is referenced by:  iffalsei  4476  iffalsed  4477  ifnefalse  4478  ifsb  4479  ifbi  4487  ifeq1da  4496  ifeq12da  4498  ifclda  4500  ifeqda  4501  elimif  4502  ifbothda  4503  ifid  4505  ifnot  4516  ifan  4517  ifor  4518  2if2  4519  ifcomnan  4520  elimhyp  4529  elimhyp2v  4530  elimhyp3v  4531  elimhyp4v  4532  elimdhyp  4534  keephyp2v  4536  keephyp3v  4537  dfopif  4799  opprc  4825  somin1  5992  elimdelov  7249  ovif12  7252  oevn0  8139  pw2f1olem  8620  unxpdomlem2  8722  unxpdomlem3  8723  infsupprpr  8967  oi0  8991  wemaplem2  9010  ixpiunwdom  9054  cantnfp1lem3  9142  cantnflem1  9151  dfac12lem2  9569  fin23lem14  9754  axcc2lem  9857  ttukeylem5  9934  uzin  12277  xrmax1  12567  xrmax2  12568  xrmin1  12569  xrmin2  12570  max1ALT  12578  ifle  12589  xmulneg1  12661  modifeq2int  13300  seqf1olem1  13408  seqf1olem2  13409  bcval3  13665  swrdccat  14096  pfxccat3a  14099  swrdccat3b  14101  repswswrd  14145  cshword  14152  ccatco  14196  sumrblem  15067  fsumcvg  15068  summolem2a  15071  sumss  15080  fsumcvg2  15083  sumsplit  15122  prodeq2ii  15266  prodrblem  15282  fprodcvg  15283  prodmolem2a  15287  zprod  15290  prodss  15300  ruclem2  15584  ruclem3  15585  flodddiv4  15763  sadadd2lem2  15798  sadcp1  15803  sadcaddlem  15805  gcdn0val  15846  dfgcd2  15893  lcmn0val  15938  lcmfn0val  15966  pcgcd  16213  pcmptcl  16226  pcmpt  16227  pcmpt2  16228  pcprod  16230  fldivp1  16232  prmreclem2  16252  prmreclem4  16254  vdwlem6  16321  prmop1  16373  fvprmselelfz  16379  fvprmselgcd1  16380  ressval2  16552  xpsaddlem  16845  xpsvsca  16849  mreexexd  16918  setcepi  17347  pmtrmvd  18583  fincygsubgodd  19233  mvrf1  20204  mplcoe3  20246  mplmon2  20272  psrbagsn  20274  evlslem1  20294  obselocv  20871  dmatmul  21105  1mavmul  21156  mulmarep1gsum2  21182  1marepvmarrepid  21183  mdetdiag  21207  mdetrsca2  21212  mdetrlin2  21215  mdetunilem5  21224  mdetunilem7  21226  mdetunilem8  21227  mdetunilem9  21228  mndifsplit  21244  maducoeval2  21248  madugsum  21251  madurid  21252  smadiadetglem2  21280  1elcpmat  21322  decpmatid  21377  ptpjpre1  22178  ptbasfi  22188  isfcls  22616  ptcmplem2  22660  ptcmplem3  22661  dscmet  23181  dscopn  23182  icccmplem2  23430  cnmpopc  23531  iccpnfcnv  23547  xrhmeo  23549  pcoval2  23619  pcopt  23625  pcopt2  23626  pcoass  23627  pcorevlem  23629  i1f1lem  24289  itg1addlem2  24297  itg1addlem3  24298  i1fres  24305  itg1climres  24314  mbfi1fseqlem4  24318  mbfi1fseqlem5  24319  itg2const2  24341  itg2seq  24342  itg2uba  24343  itg2splitlem  24348  itg2split  24349  itg2monolem1  24350  itg2gt0  24360  itg2cnlem1  24361  itg2cnlem2  24362  iblss  24404  iblss2  24405  itgle  24409  itgss  24411  ibladdlem  24419  itgaddlem1  24422  iblabslem  24427  iblabs  24428  iblabsr  24429  iblmulc2  24430  bddmulibl  24438  ditgneg  24454  elply2  24785  coeeq2  24831  dgrle  24832  coe1termlem  24847  logcnlem3  25226  igamgam  25625  isppw  25690  isnsqf  25711  mule1  25724  sqff1o  25758  chtublem  25786  dchrelbasd  25814  bposlem1  25859  bposlem3  25861  bposlem5  25863  bposlem6  25864  lgsneg  25896  lgsdilem  25899  lgsdir2  25905  lgsdir  25907  lgsdi  25909  lgsne0  25910  gausslemma2dlem1a  25940  2lgslem1c  25968  2lgs  25982  dchrvmasum2if  26072  ostth2lem4  26211  axlowdimlem15  26741  elimifd  30297  elim2if  30298  ifeq3da  30300  imadifxp  30350  pmtridf1o  30736  resvval2  30902  xrge0iifcnv  31176  indval2  31273  ddeval0  31494  eulerpartlemb  31626  plymulx0  31817  signsw0glem  31823  signswmnd  31827  dfrdg2  33040  dfrdg3  33041  noprefixmo  33202  nosupno  33203  nosupdm  33204  nosupbday  33205  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  unisnif  33386  dfrdg4  33412  bj-xpima1sn  34268  finxpreclem2  34670  finxpreclem5  34675  matunitlindflem1  34887  poimirlem15  34906  poimirlem23  34914  mbfposadd  34938  itg2addnclem  34942  itg2addnclem3  34944  itg2gt0cn  34946  ibladdnclem  34947  itgaddnclem1  34949  iblabsnclem  34954  iblabsnc  34955  iblmulc2nc  34956  bddiblnc  34961  ftc1anclem5  34970  ftc1anclem7  34972  ftc1anclem8  34973  ftc1anc  34974  areacirclem5  34985  areacirc  34986  heiborlem4  35091  ac6s6  35449  riotaclbgBAD  36089  cdleme27a  37502  cdleme31sn2  37524  dihvalc  38368  mapdhval2  38861  hdmap1val2  38935  dffltz  39269  pw2f1ocnv  39632  aomclem5  39656  arearect  39820  areaquad  39821  upbdrech2  41573  lptioo2  41910  lptioo1  41911  limsupmnfuzlem  42005  limsupre3uzlem  42014  limsup10exlem  42051  coskpi2  42145  cosknegpi  42148  icccncfext  42168  cncfiooicclem1  42174  cncfiooiccre  42176  ioodvbdlimc1lem2  42215  ioodvbdlimc2lem  42217  itgioocnicc  42260  iblcncfioo  42261  volico  42267  sublevolico  42268  voliooico  42276  voliccico  42283  dirkerper  42380  dirkertrigeq  42385  dirkercncflem2  42388  fourierdlem10  42401  fourierdlem32  42423  fourierdlem33  42424  fourierdlem37  42428  fourierdlem62  42452  fourierdlem73  42463  fourierdlem74  42464  fourierdlem75  42465  fourierdlem79  42469  fourierdlem81  42471  fourierdlem82  42472  fourierdlem93  42483  fourierdlem97  42487  fourierdlem101  42491  fourierdlem103  42493  fourierdlem104  42494  sqwvfoura  42512  sqwvfourb  42513  fourierswlem  42514  fouriersw  42515  elaa2lem  42517  etransclem15  42533  etransclem19  42537  etransclem23  42541  etransclem24  42542  etransclem25  42543  ioorrnopnxrlem  42590  nnfoctbdjlem  42736  isomenndlem  42811  ovn0  42847  hsphoidmvle2  42866  hoidmv1lelem1  42872  hoidmv1lelem2  42873  hoidmv1le  42875  hoidmvlelem2  42877  hoidmvlelem3  42878  ovnhoilem1  42882  hspdifhsp  42897  hoidifhspdmvle  42901  hspmbllem1  42907  hspmbllem2  42908  hspmbl  42910  volico2  42922  ovolval4lem2  42931  ovolval5lem1  42933  afvnfundmuv  43337  ndfatafv2  43409  prproropf1olem4  43667  suppmptcfin  44426  linc1  44479  ifnmfalse  44861