Theorem iffalse 4483

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113  {cab 2711  ifcif 4474

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4475

This theorem is referenced by:  iffalsei  4484  iffalsed  4485  ifnefalse  4486  iftrueb  4487  ifsb  4488  ifbi  4497  ifeq1da  4506  ifeq12da  4508  ifclda  4510  ifeqda  4511  elimif  4512  ifbothda  4513  ifid  4515  ifnot  4527  ifan  4528  ifor  4529  2if2  4530  ifcomnan  4531  elimhyp  4540  elimhyp2v  4541  elimhyp3v  4542  elimhyp4v  4543  elimdhyp  4545  keephyp2v  4547  keephyp3v  4548  dfopif  4821  opprc  4847  somin1  6084  elimdelov  7448  brif1  7449  ovif12  7452  ifmpt2v  7454  oevn0  8436  pw2f1olem  9001  unxpdomlem2  9148  unxpdomlem3  9149  infsupprpr  9397  oi0  9421  wemaplem2  9440  ixpiunwdom  9483  cantnfp1lem3  9577  cantnflem1  9586  dfac12lem2  10043  fin23lem14  10231  axcc2lem  10334  ttukeylem5  10411  uzin  12774  xrmax1  13076  xrmax2  13077  xrmin1  13078  xrmin2  13079  max1ALT  13087  ifle  13098  xmulneg1  13170  modifeq2int  13842  seqf1olem1  13950  seqf1olem2  13951  bcval3  14215  swrdccat  14644  pfxccat3a  14647  swrdccat3b  14649  repswswrd  14693  cshword  14700  ccatco  14744  sumrblem  15620  fsumcvg  15621  summolem2a  15624  sumss  15633  fsumcvg2  15636  sumsplit  15677  prodeq2ii  15820  prodrblem  15838  fprodcvg  15839  prodmolem2a  15843  zprod  15846  prodss  15856  ruclem2  16143  ruclem3  16144  flodddiv4  16328  sadadd2lem2  16363  sadcp1  16368  sadcaddlem  16370  gcdn0val  16411  dfgcd2  16459  lcmn0val  16508  lcmfn0val  16536  pcgcd  16792  pcmptcl  16805  pcmpt  16806  pcmpt2  16807  pcprod  16809  fldivp1  16811  prmreclem2  16831  prmreclem4  16833  vdwlem6  16900  prmop1  16952  fvprmselelfz  16958  fvprmselgcd1  16959  ressval2  17148  xpsaddlem  17479  xpsvsca  17483  mreexexd  17556  setcepi  17997  pmtrmvd  19370  fincygsubgodd  20028  obselocv  21667  mvrf1  21924  mplcoe3  21974  mplmon2  21997  psrbagsn  21999  evlslem1  22018  mhpsclcl  22063  mhpvarcl  22064  dmatmul  22413  1mavmul  22464  mulmarep1gsum2  22490  1marepvmarrepid  22491  mdetdiag  22515  mdetrsca2  22520  mdetrlin2  22523  mdetunilem5  22532  mdetunilem7  22534  mdetunilem8  22535  mdetunilem9  22536  mndifsplit  22552  maducoeval2  22556  madugsum  22559  madurid  22560  smadiadetglem2  22588  1elcpmat  22631  decpmatid  22686  ptpjpre1  23487  ptbasfi  23497  isfcls  23925  ptcmplem2  23969  ptcmplem3  23970  dscmet  24488  dscopn  24489  icccmplem2  24740  cnmpopc  24850  iccpnfcnv  24870  xrhmeo  24872  pcoval2  24944  pcopt  24950  pcopt2  24951  pcoass  24952  pcorevlem  24954  i1f1lem  25618  itg1addlem2  25626  itg1addlem3  25627  i1fres  25634  itg1climres  25643  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  itg2const2  25670  itg2seq  25671  itg2uba  25672  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  iblss  25734  iblss2  25735  itgle  25739  itgss  25741  ibladdlem  25749  itgaddlem1  25752  iblabslem  25757  iblabs  25758  iblabsr  25759  iblmulc2  25760  bddmulibl  25768  bddiblnc  25771  ditgneg  25786  elply2  26129  coeeq2  26175  dgrle  26176  coe1termlem  26191  logcnlem3  26581  igamgam  26987  isppw  27052  isnsqf  27073  mule1  27086  sqff1o  27120  chtublem  27150  dchrelbasd  27178  bposlem1  27223  bposlem3  27225  bposlem5  27227  bposlem6  27228  lgsneg  27260  lgsdilem  27263  lgsdir2  27269  lgsdir  27271  lgsdi  27273  lgsne0  27274  gausslemma2dlem1a  27304  2lgslem1c  27332  2lgs  27346  dchrvmasum2if  27436  ostth2lem4  27575  nosupno  27643  nosupdm  27644  nosupbday  27645  nosupfv  27646  nosupres  27647  nosupbnd1lem1  27648  noinfno  27658  noinfdm  27659  noinffv  27661  maxs1  27705  maxs2  27706  mins1  27707  mins2  27708  abssnid  28182  abssge0  28184  axlowdimlem15  28936  elimifd  32525  elim2if  32526  ifeq3da  32528  ifnetrue  32529  imadifxp  32583  indval2  32840  pmtridf1o  33070  resvval2  33303  xrge0iifcnv  33967  ddeval0  34269  eulerpartlemb  34402  plymulx0  34581  signsw0glem  34587  signswmnd  34591  dfrdg2  35858  dfrdg3  35859  unisnif  35988  dfrdg4  36016  bj-xpima1sn  37021  finxpreclem2  37455  finxpreclem5  37460  matunitlindflem1  37677  poimirlem15  37696  poimirlem23  37704  mbfposadd  37728  itg2addnclem  37732  itg2addnclem3  37734  itg2gt0cn  37736  ibladdnclem  37737  itgaddnclem1  37739  iblabsnclem  37744  iblabsnc  37745  iblmulc2nc  37746  ftc1anclem5  37758  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  areacirclem5  37773  areacirc  37774  heiborlem4  37875  ac6s6  38233  riotaclbgBAD  39074  cdleme27a  40487  cdleme31sn2  40509  dihvalc  41353  mapdhval2  41846  hdmap1val2  41920  brif2  42343  brif12  42344  fsuppind  42709  dffltz  42753  pw2f1ocnv  43155  aomclem5  43176  arearect  43333  areaquad  43334  safesnsupfidom1o  43535  safesnsupfilb  43536  upbdrech2  45434  lptioo2  45756  lptioo1  45757  limsupmnfuzlem  45849  limsupre3uzlem  45858  limsup10exlem  45895  coskpi2  45989  cosknegpi  45992  icccncfext  46010  cncfiooicclem1  46016  cncfiooiccre  46018  ioodvbdlimc1lem2  46055  ioodvbdlimc2lem  46057  itgioocnicc  46100  iblcncfioo  46101  volico  46106  sublevolico  46107  voliooico  46115  voliccico  46122  dirkerper  46219  dirkertrigeq  46224  dirkercncflem2  46227  fourierdlem10  46240  fourierdlem32  46262  fourierdlem33  46263  fourierdlem37  46267  fourierdlem62  46291  fourierdlem73  46302  fourierdlem74  46303  fourierdlem75  46304  fourierdlem79  46308  fourierdlem81  46310  fourierdlem82  46311  fourierdlem93  46322  fourierdlem97  46326  fourierdlem101  46330  fourierdlem103  46332  fourierdlem104  46333  sqwvfoura  46351  sqwvfourb  46352  fourierswlem  46353  fouriersw  46354  elaa2lem  46356  etransclem15  46372  etransclem19  46376  etransclem23  46380  etransclem24  46381  etransclem25  46382  ioorrnopnxrlem  46429  nnfoctbdjlem  46578  isomenndlem  46653  ovn0  46689  hsphoidmvle2  46708  hoidmv1lelem1  46714  hoidmv1lelem2  46715  hoidmv1le  46717  hoidmvlelem2  46719  hoidmvlelem3  46720  ovnhoilem1  46724  hspdifhsp  46739  hoidifhspdmvle  46743  hspmbllem1  46749  hspmbllem2  46750  hspmbl  46752  volico2  46764  ovolval4lem2  46773  ovolval5lem1  46775  afvnfundmuv  47264  ndfatafv2  47336  difmodm1lt  47484  prproropf1olem4  47631  suppmptcfin  48501  linc1  48551  discsubc  49190  oppfrcl3  49256  eloppf  49259  eloppf2  49260  ifnmfalse  49889