Theorem iffalse 4539

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1536   ∈ wcel 2105  {cab 2711  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  iffalsei  4540  iffalsed  4541  ifnefalse  4542  ifsb  4543  ifbi  4552  ifeq1da  4561  ifeq12da  4563  ifclda  4565  ifeqda  4566  elimif  4567  ifbothda  4568  ifid  4570  ifnot  4582  ifan  4583  ifor  4584  2if2  4585  ifcomnan  4586  elimhyp  4595  elimhyp2v  4596  elimhyp3v  4597  elimhyp4v  4598  elimdhyp  4600  keephyp2v  4602  keephyp3v  4603  dfopif  4874  opprc  4900  somin1  6155  elimdelov  7528  brif1  7529  ovif12  7532  oevn0  8551  pw2f1olem  9114  unxpdomlem2  9284  unxpdomlem3  9285  infsupprpr  9541  oi0  9565  wemaplem2  9584  ixpiunwdom  9627  cantnfp1lem3  9717  cantnflem1  9726  dfac12lem2  10182  fin23lem14  10370  axcc2lem  10473  ttukeylem5  10550  uzin  12915  xrmax1  13213  xrmax2  13214  xrmin1  13215  xrmin2  13216  max1ALT  13224  ifle  13235  xmulneg1  13307  modifeq2int  13970  seqf1olem1  14078  seqf1olem2  14079  bcval3  14341  swrdccat  14769  pfxccat3a  14772  swrdccat3b  14774  repswswrd  14818  cshword  14825  ccatco  14870  sumrblem  15743  fsumcvg  15744  summolem2a  15747  sumss  15756  fsumcvg2  15759  sumsplit  15800  prodeq2ii  15943  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  prodss  15979  ruclem2  16264  ruclem3  16265  flodddiv4  16448  sadadd2lem2  16483  sadcp1  16488  sadcaddlem  16490  gcdn0val  16531  dfgcd2  16579  lcmn0val  16628  lcmfn0val  16656  pcgcd  16911  pcmptcl  16924  pcmpt  16925  pcmpt2  16926  pcprod  16928  fldivp1  16930  prmreclem2  16950  prmreclem4  16952  vdwlem6  17019  prmop1  17071  fvprmselelfz  17077  fvprmselgcd1  17078  ressval2  17278  xpsaddlem  17619  xpsvsca  17623  mreexexd  17692  setcepi  18141  pmtrmvd  19488  fincygsubgodd  20146  obselocv  21765  mvrf1  22023  mplcoe3  22073  mplmon2  22102  psrbagsn  22104  evlslem1  22123  mhpsclcl  22168  mhpvarcl  22169  dmatmul  22518  1mavmul  22569  mulmarep1gsum2  22595  1marepvmarrepid  22596  mdetdiag  22620  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  mdetunilem7  22639  mdetunilem8  22640  mdetunilem9  22641  mndifsplit  22657  maducoeval2  22661  madugsum  22664  madurid  22665  smadiadetglem2  22693  1elcpmat  22736  decpmatid  22791  ptpjpre1  23594  ptbasfi  23604  isfcls  24032  ptcmplem2  24076  ptcmplem3  24077  dscmet  24600  dscopn  24601  icccmplem2  24858  cnmpopc  24968  iccpnfcnv  24988  xrhmeo  24990  pcoval2  25062  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  i1f1lem  25737  itg1addlem2  25745  itg1addlem3  25746  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  iblss  25854  iblss2  25855  itgle  25859  itgss  25861  ibladdlem  25869  itgaddlem1  25872  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  bddmulibl  25888  bddiblnc  25891  ditgneg  25906  elply2  26249  coeeq2  26295  dgrle  26296  coe1termlem  26311  logcnlem3  26700  igamgam  27106  isppw  27171  isnsqf  27192  mule1  27205  sqff1o  27239  chtublem  27269  dchrelbasd  27297  bposlem1  27342  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgsneg  27379  lgsdilem  27382  lgsdir2  27388  lgsdir  27390  lgsdi  27392  lgsne0  27393  gausslemma2dlem1a  27423  2lgslem1c  27451  2lgs  27465  dchrvmasum2if  27555  ostth2lem4  27694  nosupno  27762  nosupdm  27763  nosupbday  27764  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  noinfno  27777  noinfdm  27778  noinffv  27780  maxs1  27824  maxs2  27825  mins1  27826  mins2  27827  abssnid  28281  abssge0  28283  axlowdimlem15  28985  elimifd  32563  elim2if  32564  ifeq3da  32566  ifnetrue  32567  imadifxp  32620  pmtridf1o  33096  resvval2  33334  xrge0iifcnv  33893  indval2  33994  ddeval0  34215  eulerpartlemb  34349  plymulx0  34540  signsw0glem  34546  signswmnd  34550  dfrdg2  35776  dfrdg3  35777  unisnif  35906  dfrdg4  35932  bj-xpima1sn  36938  finxpreclem2  37372  finxpreclem5  37377  matunitlindflem1  37602  poimirlem15  37621  poimirlem23  37629  mbfposadd  37653  itg2addnclem  37657  itg2addnclem3  37659  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem1  37664  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirclem5  37698  areacirc  37699  heiborlem4  37800  ac6s6  38158  riotaclbgBAD  38935  cdleme27a  40349  cdleme31sn2  40371  dihvalc  41215  mapdhval2  41708  hdmap1val2  41782  metakunt6  42191  metakunt7  42192  metakunt8  42193  metakunt11  42196  metakunt12  42197  metakunt22  42207  brif2  42241  brif12  42242  fsuppind  42576  dffltz  42620  pw2f1ocnv  43025  aomclem5  43046  arearect  43203  areaquad  43204  safesnsupfidom1o  43406  safesnsupfilb  43407  upbdrech2  45258  lptioo2  45586  lptioo1  45587  limsupmnfuzlem  45681  limsupre3uzlem  45690  limsup10exlem  45727  coskpi2  45821  cosknegpi  45824  icccncfext  45842  cncfiooicclem1  45848  cncfiooiccre  45850  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  itgioocnicc  45932  iblcncfioo  45933  volico  45938  sublevolico  45939  voliooico  45947  voliccico  45954  dirkerper  46051  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem10  46072  fourierdlem32  46094  fourierdlem33  46095  fourierdlem37  46099  fourierdlem62  46123  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem93  46154  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem15  46204  etransclem19  46208  etransclem23  46212  etransclem24  46213  etransclem25  46214  ioorrnopnxrlem  46261  nnfoctbdjlem  46410  isomenndlem  46485  ovn0  46521  hsphoidmvle2  46540  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1le  46549  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  hspdifhsp  46571  hoidifhspdmvle  46575  hspmbllem1  46581  hspmbllem2  46582  hspmbl  46584  volico2  46596  ovolval4lem2  46605  ovolval5lem1  46607  afvnfundmuv  47088  ndfatafv2  47160  prproropf1olem4  47430  suppmptcfin  48220  linc1  48270  ifnmfalse  48993