Theorem iffalse 4492

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1563   ∈ wcel 2145  {cab 2743  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  iffalsei  4493  iffalsed  4494  ifnefalse  4495  iftrueb  4496  ifsb  4497  ifbi  4506  ifeq1da  4515  ifeq12da  4517  ifclda  4519  ifeqda  4520  elimif  4521  ifbothda  4522  ifid  4524  ifnot  4536  ifan  4537  ifor  4538  2if2  4539  ifcomnan  4540  elimhyp  4549  elimhyp2v  4550  elimhyp3v  4551  elimhyp4v  4552  elimdhyp  4554  keephyp2v  4556  keephyp3v  4557  dfopif  4831  opprc  4857  somin1  6124  elimdelov  7496  brif1  7497  ovif12  7500  ifmpt2v  7502  oevn0  8488  pw2f1olem  9057  unxpdomlem2  9205  unxpdomlem3  9206  infsupprpr  9454  oi0  9478  wemaplem2  9497  ixpiunwdom  9540  cantnfp1lem3  9637  cantnflem1  9646  dfac12lem2  10116  fin23lem14  10305  axcc2lem  10408  ttukeylem5  10485  indval2  12214  uzin  12889  xrmax1  13192  xrmax2  13193  xrmin1  13194  xrmin2  13195  max1ALT  13203  ifle  13214  xmulneg1  13286  modifeq2int  13960  seqf1olem1  14068  seqf1olem2  14069  bcval3  14333  swrdccat  14762  pfxccat3a  14765  swrdccat3b  14767  repswswrd  14811  cshword  14818  ccatco  14862  sumrblem  15752  fsumcvg  15753  summolem2a  15756  sumss  15765  fsumcvg2  15768  sumsplit  15809  prodeq2ii  15955  prodrblem  15973  fprodcvg  15974  prodmolem2a  15978  zprod  15981  prodss  15991  ruclem2  16278  ruclem3  16279  flodddiv4  16463  sadadd2lem2  16498  sadcp1  16503  sadcaddlem  16505  gcdn0val  16546  dfgcd2  16594  lcmn0val  16643  lcmfn0val  16671  pcgcd  16928  pcmptcl  16941  pcmpt  16942  pcmpt2  16943  pcprod  16945  fldivp1  16947  prmreclem2  16967  prmreclem4  16969  vdwlem6  17036  prmop1  17088  fvprmselelfz  17094  fvprmselgcd1  17095  ressval2  17285  xpsaddlem  17617  xpsvsca  17621  mreexexd  17694  setcepi  18135  pmtrmvd  19517  fincygsubgodd  20175  obselocv  21838  mvrf1  22095  mplcoe3  22149  mplmon2  22172  psrbagsn  22174  evlslem1  22193  mhpsclcl  22270  mhpvarcl  22271  dmatmul  22615  1mavmul  22666  mulmarep1gsum2  22692  1marepvmarrepid  22693  mdetdiag  22717  mdetrsca2  22722  mdetrlin2  22725  mdetunilem5  22734  mdetunilem7  22736  mdetunilem8  22737  mdetunilem9  22738  mndifsplit  22754  maducoeval2  22758  madugsum  22761  madurid  22762  smadiadetglem2  22790  1elcpmat  22833  decpmatid  22888  ptpjpre1  23689  ptbasfi  23699  isfcls  24127  ptcmplem2  24171  ptcmplem3  24172  dscmet  24690  dscopn  24691  icccmplem2  24942  cnmpopc  25048  iccpnfcnv  25064  xrhmeo  25066  pcoval2  25136  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  i1f1lem  25809  itg1addlem2  25817  itg1addlem3  25818  i1fres  25825  itg1climres  25834  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  itg2const2  25861  itg2seq  25862  itg2uba  25863  itg2splitlem  25868  itg2split  25869  itg2monolem1  25870  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  iblss  25925  iblss2  25926  itgle  25930  itgss  25932  ibladdlem  25940  itgaddlem1  25943  iblabslem  25948  iblabs  25949  iblabsr  25950  iblmulc2  25951  bddmulibl  25959  bddiblnc  25962  ditgneg  25977  elply2  26314  coeeq2  26360  dgrle  26361  coe1termlem  26376  plyn0mulidp  26403  logcnlem3  26767  igamgam  27171  isppw  27236  isnsqf  27257  mule1  27270  sqff1o  27304  chtublem  27333  dchrelbasd  27361  bposlem1  27406  bposlem3  27408  bposlem5  27410  bposlem6  27411  lgsneg  27443  lgsdilem  27446  lgsdir2  27452  lgsdir  27454  lgsdi  27456  lgsne0  27457  gausslemma2dlem1a  27487  2lgslem1c  27515  2lgs  27529  dchrvmasum2if  27619  ostth2lem4  27758  nosupno  27825  nosupdm  27826  nosupbday  27827  nosupfv  27828  nosupres  27829  nosupbnd1lem1  27830  noinfno  27840  noinfdm  27841  noinffv  27843  maxs1  27891  maxs2  27892  mins1  27893  mins2  27894  abssnid  28394  abssge0  28396  axlowdimlem15  29215  elimifd  32799  elim2if  32800  ifeq3da  32802  ifnetrue  32803  imadifxp  32856  pmtridf1o  33327  resvval2  33566  xrge0iifcnv  34240  ddeval0  34542  eulerpartlemb  34675  signsw0glem  34857  signswmnd  34861  vonf1oonfo  35470  dfrdg2  36156  dfrdg3  36157  unisnif  36286  dfrdg4  36314  bj-xpima1sn  37453  finxpreclem2  37896  finxpreclem5  37901  matunitlindflem1  38127  poimirlem15  38146  poimirlem23  38154  mbfposadd  38178  itg2addnclem  38182  itg2addnclem3  38184  itg2gt0cn  38186  ibladdnclem  38187  itgaddnclem1  38189  iblabsnclem  38194  iblabsnc  38195  iblmulc2nc  38196  ftc1anclem5  38208  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  areacirclem5  38223  areacirc  38224  heiborlem4  38325  ac6s6  38683  riotaclbgBAD  39590  cdleme27a  41003  cdleme31sn2  41025  dihvalc  41869  mapdhval2  42362  hdmap1val2  42436  brif2  42855  brif12  42856  fsuppind  43184  dffltz  43228  pw2f1ocnv  43626  aomclem5  43647  arearect  43804  areaquad  43805  safesnsupfidom1o  44005  safesnsupfilb  44006  upbdrech2  45885  lptioo2  46205  lptioo1  46206  limsupmnfuzlem  46298  limsupre3uzlem  46307  limsup10exlem  46344  coskpi2  46438  cosknegpi  46441  icccncfext  46459  cncfiooicclem1  46465  cncfiooiccre  46467  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  itgioocnicc  46549  iblcncfioo  46550  volico  46555  sublevolico  46556  voliooico  46564  voliccico  46571  dirkerper  46668  dirkertrigeq  46673  dirkercncflem2  46676  fourierdlem10  46689  fourierdlem32  46711  fourierdlem33  46712  fourierdlem37  46716  fourierdlem62  46740  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem79  46757  fourierdlem81  46759  fourierdlem82  46760  fourierdlem93  46771  fourierdlem97  46775  fourierdlem101  46779  fourierdlem103  46781  fourierdlem104  46782  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  elaa2lem  46805  etransclem15  46821  etransclem19  46825  etransclem23  46829  etransclem24  46830  etransclem25  46831  ioorrnopnxrlem  46878  nnfoctbdjlem  47027  isomenndlem  47102  ovn0  47138  hsphoidmvle2  47157  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmv1le  47166  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoilem1  47173  hspdifhsp  47188  hoidifhspdmvle  47192  hspmbllem1  47198  hspmbllem2  47199  hspmbl  47201  volico2  47213  ovolval4lem2  47222  ovolval5lem1  47224  afvnfundmuv  47731  ndfatafv2  47803  difmodm1lt  47957  prproropf1olem4  48110  suppmptcfin  49007  linc1  49056  discsubc  49693  oppfrcl3  49759  eloppf  49762  eloppf2  49763  ifnmfalse  50392