MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iftrue Structured version   Visualization version   GIF version

Theorem iftrue 4236
Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
iftrue (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Proof of Theorem iftrue
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dedlem0a 1030 . . 3 (𝜑 → (𝑥𝐴 ↔ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))))
21abbi2dv 2880 . 2 (𝜑𝐴 = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))})
3 dfif2 4232 . 2 if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥𝐵𝜑) → (𝑥𝐴𝜑))}
42, 3syl6reqr 2813 1 (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  {cab 2746  ifcif 4230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-if 4231
This theorem is referenced by:  iftruei  4237  iftrued  4238  ifsb  4243  ifbi  4251  ifeq2da  4261  ifeq12da  4262  ifclda  4264  ifeqda  4265  elimif  4266  ifbothda  4267  ifid  4269  ifeqor  4276  ifnot  4277  ifan  4278  ifor  4279  2if2  4280  dedth  4283  elimhyp  4290  elimhyp2v  4291  elimhyp3v  4292  elimhyp4v  4293  elimdhyp  4295  keephyp2v  4297  keephyp3v  4298  dfopif  4550  dfopg  4551  somin1  5687  somincom  5688  xpima1  5735  dfiota4OLD  6041  elimdelov  6902  ovif12  6905  tz7.44-1  7672  resixpfo  8114  boxriin  8118  boxcutc  8119  pw2f1olem  8231  unxpdomlem2  8332  unxpdomlem3  8333  ordtypelem1  8590  wemaplem2  8619  unwdomg  8656  ixpiunwdom  8663  cantnfp1lem2  8751  cantnfp1lem3  8752  acndom  9084  dfac12lem2  9178  fin23lem14  9367  axcc2lem  9470  pwfseqlem2  9693  uzin  11933  xrmax1  12219  xrmax2  12220  xrmin1  12221  xrmin2  12222  max1ALT  12230  max0sub  12240  ifle  12241  xmulneg1  12312  fzprval  12614  fztpval  12615  modifeq2int  12946  seqf1olem1  13054  seqf1olem2  13055  bcval2  13306  ccatval1  13569  ccatalpha  13585  swrdccat  13713  swrdccat3a  13714  swrdccat3b  13716  repswswrd  13751  cshword  13757  0csh0  13759  ccatco  13801  sgnn  14053  max0add  14269  absmax  14288  sumrblem  14661  fsumcvg  14662  summolem2a  14665  isum  14669  sumss  14674  sumss2  14676  fsumcvg2  14677  fsumser  14680  fsumsplit  14690  sumsplit  14718  prodrblem  14878  fprodcvg  14879  prodmolem2a  14883  zprod  14886  iprod  14887  iprodn0  14889  prodss  14896  fprodsplit  14915  ruclem2  15180  ruclem3  15181  flodddiv4  15359  sadadd2lem2  15394  sadcf  15397  sadc0  15398  sadcp1  15399  sadcaddlem  15401  smupf  15422  smup0  15423  gcd0val  15441  dfgcd2  15485  eucalgf  15518  eucalginv  15519  eucalglt  15520  lcmf0val  15557  phisum  15717  pc0  15781  pcgcd  15804  pcmptcl  15817  pcmpt  15818  pcmpt2  15819  pcprod  15821  fldivp1  15823  prmreclem2  15843  prmreclem4  15845  1arithlem4  15852  vdwlem6  15912  ramtcl2  15937  ramcl2  15942  ramub1lem1  15952  prmop1  15964  fvprmselelfz  15970  fvprmselgcd1  15971  ressid2  16150  xpscfv  16444  xpsfrnel  16445  xpsaddlem  16457  xpsvsca  16461  mreexexd  16530  gsumval1  17498  mgm2nsgrplem2  17627  sgrp2nmndlem2  17632  symgextfve  18059  symgfixfolem1  18078  pmtrmvd  18096  pmtrfinv  18101  pmtrprfval  18127  pmtrprfvalrn  18128  frgpuptinv  18404  frgpup2  18409  frgpup3lem  18410  cyggex  18519  gsumzsplit  18547  gsummpt1n0  18584  dprdfid  18636  dmdprdsplitlem  18656  abvtrivd  19062  psrlidm  19625  psrridm  19626  mvrf1  19647  mplmonmul  19686  mplcoe1  19687  mplcoe3  19688  mplcoe5  19690  mplmon2  19715  subrgasclcl  19721  evlslem3  19736  evlslem1  19737  coe1tmfv1  19866  ply1sclid  19880  znf1o  20122  uvcvv1  20350  dmatmul  20525  scmatscmiddistr  20536  1mavmul  20576  mulmarep1gsum2  20602  1marepvmarrepid  20603  mdetdiag  20627  mdetralt2  20637  mdetunilem2  20641  mdetunilem7  20646  mdetunilem8  20647  mdetunilem9  20648  mndifsplit  20664  maducoeval2  20668  madugsum  20671  madurid  20672  gsummatr01lem3  20685  gsummatr01  20687  smadiadetglem2  20700  1elcpmat  20742  decpmatid  20797  chfacfscmulgsum  20887  chfacfpmmulgsum  20891  ptpjpre1  21596  ptbasfi  21606  ptpjopn  21637  isfcls  22034  ptcmplem2  22078  ptcmplem3  22079  tsmssplit  22176  dscmet  22598  dscopn  22599  icccmplem2  22847  iccpnfcnv  22964  xrhmeo  22966  pcohtpylem  23039  pcopt  23042  pcopt2  23043  pcoass  23044  pcorevlem  23046  cmetcaulem  23306  ovolicc1  23504  ioorcl  23565  i1f1lem  23675  itg11  23677  itg1addlem2  23683  itg1addlem4  23685  i1fres  23691  itg1climres  23700  mbfi1fseqlem4  23704  mbfi1fseqlem5  23705  mbfi1flim  23709  itg2const2  23727  itg2seq  23728  itg2uba  23729  itg2splitlem  23734  itg2split  23735  itg2monolem1  23736  itg2cnlem1  23747  itg2cnlem2  23748  iblcnlem  23774  iblss  23790  iblss2  23791  itgitg2  23792  itgle  23795  itgss  23797  itgss2  23798  itgss3  23800  itgless  23802  ibladdlem  23805  itgaddlem1  23808  iblabslem  23813  iblabs  23814  iblabsr  23815  iblmulc2  23816  bddmulibl  23824  itggt0  23827  itgcn  23828  limcvallem  23854  ellimc2  23860  limccnp  23874  limccnp2  23875  limcco  23876  dvcobr  23928  dvexp2  23936  elply2  24171  elplyd  24177  ply1termlem  24178  coe1termlem  24233  abelthlem9  24413  logtayl  24626  leibpilem2  24888  leibpi  24889  rlimcnp2  24913  efrlim  24916  igamz  24994  isnsqf  25081  mule1  25094  sqff1o  25128  muinv  25139  chtublem  25156  dchrelbasd  25184  bposlem1  25229  bposlem3  25231  bposlem5  25233  bposlem6  25234  lgsval2lem  25252  lgsneg  25266  lgsdilem  25269  lgsdir2  25275  lgsdir  25277  lgsdi  25279  lgsne0  25280  gausslemma2dlem1a  25310  2lgslem1c  25338  2lgslem3  25349  2lgs  25352  dchrvmasum2if  25406  dchrvmasumiflem1  25410  rpvmasum2  25421  pntrlog2bndlem4  25489  pntrlog2bndlem5  25490  padicabv  25539  ostth2lem4  25545  axlowdimlem15  26056  opvtxval  26103  opiedgval  26106  elimifd  29690  elim2if  29691  ifeq3da  29693  resvid2  30158  fzto1stfv1  30181  pmtridf1o  30186  xrge0iifcnv  30309  xrge0iifiso  30311  xrge0iifhom  30313  indval2  30406  ind1  30409  sigaclfu2  30514  ddeval1  30627  eulerpartlemb  30760  ballotlemsima  30907  ballotlemrv1  30912  signsw0glem  30960  signswmnd  30964  signswrid  30965  indispconn  31544  mrsubvr  31736  dfrdg2  32027  dfrdg3  32028  noprefixmo  32175  nosupno  32176  nosupbday  32178  nosupbnd1  32187  nosupbnd2  32189  unisnif  32359  dfrdg4  32385  fnejoin2  32691  unbdqndv2lem2  32828  bj-xpima2sn  33269  finxpreclem1  33555  finxpreclem3  33559  matunitlindflem1  33736  poimirlem2  33742  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem19  33759  poimirlem20  33760  poimirlem24  33764  mblfinlem2  33778  mbfposadd  33788  itg2addnclem  33792  itg2gt0cn  33796  ibladdnclem  33797  itgaddnclem1  33799  iblabsnclem  33804  iblabsnc  33805  iblmulc2nc  33806  bddiblnc  33811  itggt0cn  33813  ftc1anclem4  33819  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  areacirclem5  33835  areacirc  33836  fdc  33872  heiborlem4  33944  ac6s6  34311  cdleme27a  36175  cdleme31sn1  36189  cdleme31fv1  36199  cdlemk40t  36726  dihvalb  37046  pw2f1ocnv  38124  aomclem5  38148  kelac1  38153  sdrgacs  38291  mon1pid  38303  arearect  38321  areaquad  38322  clsk1indlem1  38863  refsum2cnlem1  39713  upbdrech2  40039  lptioo2  40384  lptioo1  40385  limsupmnfuzlem  40479  limsupre3uzlem  40488  limsup10exlem  40525  coskpi2  40598  cosknegpi  40601  cncfiooicclem1  40627  cncfiooiccre  40629  dvnxpaek  40678  dvnprodlem1  40682  dvnprodlem3  40684  itgioocnicc  40714  iblcncfioo  40715  volico  40721  sublevolico  40722  volioore  40728  voliooico  40730  voliccico  40737  dirkerper  40834  dirkertrigeq  40839  dirkercncflem2  40842  fourierdlem10  40855  fourierdlem32  40877  fourierdlem33  40878  fourierdlem37  40882  fourierdlem62  40906  fourierdlem73  40917  fourierdlem74  40918  fourierdlem75  40919  fourierdlem79  40923  fourierdlem81  40925  fourierdlem82  40926  fourierdlem93  40937  fourierdlem97  40941  fourierdlem101  40945  fourierdlem103  40947  fourierdlem104  40948  sqwvfoura  40966  sqwvfourb  40967  fourierswlem  40968  fouriersw  40969  etransclem4  40976  etransclem15  40987  etransclem19  40991  etransclem20  40992  etransclem23  40995  etransclem24  40996  etransclem25  40997  etransclem27  40999  etransclem31  41003  etransclem32  41004  ioorrnopnxrlem  41047  nnfoctbdjlem  41193  isomenndlem  41268  ovn0val  41288  hoidmv0val  41321  hsphoidmvle2  41323  hoidmv1lelem1  41329  hoidmv1lelem2  41330  hoidmv1le  41332  hoidmvlelem2  41334  hoidmvlelem3  41335  ovnhoilem1  41339  hspdifhsp  41354  hoidifhspdmvle  41358  hspmbllem1  41364  hspmbllem2  41365  hspmbl  41367  volico2  41379  ovnsubadd2lem  41383  ovolval4lem2  41388  ovolval5lem1  41390  afvfundmfveq  41742  pfxccat3a  41957  cshword2  41965  linc1  42742  lincext3  42773  lindslinindsimp1  42774  el0ldep  42783  islindeps2  42800
  Copyright terms: Public domain W3C validator