Theorem iffalse 4490

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114  {cab 2715  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  iffalsei  4491  iffalsed  4492  ifnefalse  4493  iftrueb  4494  ifsb  4495  ifbi  4504  ifeq1da  4513  ifeq12da  4515  ifclda  4517  ifeqda  4518  elimif  4519  ifbothda  4520  ifid  4522  ifnot  4534  ifan  4535  ifor  4536  2if2  4537  ifcomnan  4538  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  dfopif  4828  opprc  4854  somin1  6098  elimdelov  7464  brif1  7465  ovif12  7468  ifmpt2v  7470  oevn0  8452  pw2f1olem  9021  unxpdomlem2  9169  unxpdomlem3  9170  infsupprpr  9421  oi0  9445  wemaplem2  9464  ixpiunwdom  9507  cantnfp1lem3  9601  cantnflem1  9610  dfac12lem2  10067  fin23lem14  10255  axcc2lem  10358  ttukeylem5  10435  uzin  12799  xrmax1  13102  xrmax2  13103  xrmin1  13104  xrmin2  13105  max1ALT  13113  ifle  13124  xmulneg1  13196  modifeq2int  13868  seqf1olem1  13976  seqf1olem2  13977  bcval3  14241  swrdccat  14670  pfxccat3a  14673  swrdccat3b  14675  repswswrd  14719  cshword  14726  ccatco  14770  sumrblem  15646  fsumcvg  15647  summolem2a  15650  sumss  15659  fsumcvg2  15662  sumsplit  15703  prodeq2ii  15846  prodrblem  15864  fprodcvg  15865  prodmolem2a  15869  zprod  15872  prodss  15882  ruclem2  16169  ruclem3  16170  flodddiv4  16354  sadadd2lem2  16389  sadcp1  16394  sadcaddlem  16396  gcdn0val  16437  dfgcd2  16485  lcmn0val  16534  lcmfn0val  16562  pcgcd  16818  pcmptcl  16831  pcmpt  16832  pcmpt2  16833  pcprod  16835  fldivp1  16837  prmreclem2  16857  prmreclem4  16859  vdwlem6  16926  prmop1  16978  fvprmselelfz  16984  fvprmselgcd1  16985  ressval2  17174  xpsaddlem  17506  xpsvsca  17510  mreexexd  17583  setcepi  18024  pmtrmvd  19397  fincygsubgodd  20055  obselocv  21695  mvrf1  21953  mplcoe3  22005  mplmon2  22028  psrbagsn  22030  evlslem1  22049  mhpsclcl  22102  mhpvarcl  22103  dmatmul  22453  1mavmul  22504  mulmarep1gsum2  22530  1marepvmarrepid  22531  mdetdiag  22555  mdetrsca2  22560  mdetrlin2  22563  mdetunilem5  22572  mdetunilem7  22574  mdetunilem8  22575  mdetunilem9  22576  mndifsplit  22592  maducoeval2  22596  madugsum  22599  madurid  22600  smadiadetglem2  22628  1elcpmat  22671  decpmatid  22726  ptpjpre1  23527  ptbasfi  23537  isfcls  23965  ptcmplem2  24009  ptcmplem3  24010  dscmet  24528  dscopn  24529  icccmplem2  24780  cnmpopc  24890  iccpnfcnv  24910  xrhmeo  24912  pcoval2  24984  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  i1f1lem  25658  itg1addlem2  25666  itg1addlem3  25667  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  itg2const2  25710  itg2seq  25711  itg2uba  25712  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  iblss  25774  iblss2  25775  itgle  25779  itgss  25781  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblabsr  25799  iblmulc2  25800  bddmulibl  25808  bddiblnc  25811  ditgneg  25826  elply2  26169  coeeq2  26215  dgrle  26216  coe1termlem  26231  logcnlem3  26621  igamgam  27027  isppw  27092  isnsqf  27113  mule1  27126  sqff1o  27160  chtublem  27190  dchrelbasd  27218  bposlem1  27263  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgsneg  27300  lgsdilem  27303  lgsdir2  27309  lgsdir  27311  lgsdi  27313  lgsne0  27314  gausslemma2dlem1a  27344  2lgslem1c  27372  2lgs  27386  dchrvmasum2if  27476  ostth2lem4  27615  nosupno  27683  nosupdm  27684  nosupbday  27685  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  noinfno  27698  noinfdm  27699  noinffv  27701  maxs1  27749  maxs2  27750  mins1  27751  mins2  27752  abssnid  28251  abssge0  28253  axlowdimlem15  29041  elimifd  32629  elim2if  32630  ifeq3da  32632  ifnetrue  32633  imadifxp  32687  indval2  32943  pmtridf1o  33187  resvval2  33423  xrge0iifcnv  34110  ddeval0  34412  eulerpartlemb  34545  plymulx0  34724  signsw0glem  34730  signswmnd  34734  dfrdg2  36006  dfrdg3  36007  unisnif  36136  dfrdg4  36164  bj-xpima1sn  37198  finxpreclem2  37639  finxpreclem5  37644  matunitlindflem1  37861  poimirlem15  37880  poimirlem23  37888  mbfposadd  37912  itg2addnclem  37916  itg2addnclem3  37918  itg2gt0cn  37920  ibladdnclem  37921  itgaddnclem1  37923  iblabsnclem  37928  iblabsnc  37929  iblmulc2nc  37930  ftc1anclem5  37942  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  areacirclem5  37957  areacirc  37958  heiborlem4  38059  ac6s6  38417  riotaclbgBAD  39324  cdleme27a  40737  cdleme31sn2  40759  dihvalc  41603  mapdhval2  42096  hdmap1val2  42170  brif2  42590  brif12  42591  fsuppind  42942  dffltz  42986  pw2f1ocnv  43388  aomclem5  43409  arearect  43566  areaquad  43567  safesnsupfidom1o  43767  safesnsupfilb  43768  upbdrech2  45664  lptioo2  45985  lptioo1  45986  limsupmnfuzlem  46078  limsupre3uzlem  46087  limsup10exlem  46124  coskpi2  46218  cosknegpi  46221  icccncfext  46239  cncfiooicclem1  46245  cncfiooiccre  46247  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  itgioocnicc  46329  iblcncfioo  46330  volico  46335  sublevolico  46336  voliooico  46344  voliccico  46351  dirkerper  46448  dirkertrigeq  46453  dirkercncflem2  46456  fourierdlem10  46469  fourierdlem32  46491  fourierdlem33  46492  fourierdlem37  46496  fourierdlem62  46520  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem79  46537  fourierdlem81  46539  fourierdlem82  46540  fourierdlem93  46551  fourierdlem97  46555  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  elaa2lem  46585  etransclem15  46601  etransclem19  46605  etransclem23  46609  etransclem24  46610  etransclem25  46611  ioorrnopnxrlem  46658  nnfoctbdjlem  46807  isomenndlem  46882  ovn0  46918  hsphoidmvle2  46937  hoidmv1lelem1  46943  hoidmv1lelem2  46944  hoidmv1le  46946  hoidmvlelem2  46948  hoidmvlelem3  46949  ovnhoilem1  46953  hspdifhsp  46968  hoidifhspdmvle  46972  hspmbllem1  46978  hspmbllem2  46979  hspmbl  46981  volico2  46993  ovolval4lem2  47002  ovolval5lem1  47004  afvnfundmuv  47493  ndfatafv2  47565  difmodm1lt  47713  prproropf1olem4  47860  suppmptcfin  48730  linc1  48779  discsubc  49417  oppfrcl3  49483  eloppf  49486  eloppf2  49487  ifnmfalse  50116