Theorem iftrue 4491

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.

Step	Hyp	Ref	Expression
1		dfif2 4487	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1059	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	eqabdv 2897	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2817	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {cab 2741  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  iftruei  4492  iftrued  4493  iftrueb  4498  ifsb  4499  ifbi  4508  ifeq2da  4518  ifeq12da  4519  ifclda  4521  ifeqda  4522  elimif  4523  ifbothda  4524  ifid  4526  ifeqor  4537  ifnot  4538  ifan  4539  ifor  4540  2if2  4541  dedth  4544  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elimdhyp  4556  keephyp2v  4558  keephyp3v  4559  dfopif  4840  dfopg  4841  somin1  6139  somincom  6140  xpima1  6187  elimdelov  7539  brif1  7540  ovif12  7543  ifmpt2v  7545  tz7.44-1  8442  rdg0n  8470  resixpfo  8992  boxriin  8996  boxcutc  8997  pw2f1olem  9128  unxpdomlem2  9276  unxpdomlem3  9277  infsupprpr  9525  ordtypelem1  9539  wemaplem2  9568  unwdomg  9605  ixpiunwdom  9611  cantnfp1lem2  9707  cantnfp1lem3  9708  ssttrcl  9743  ttrclselem2  9754  acndom  10157  dfac12lem2  10250  fin23lem14  10438  axcc2lem  10541  pwfseqlem2  10771  indval2  12352  ind1  12356  uzin  13028  xrmax1  13332  xrmax2  13333  xrmin1  13334  xrmin2  13335  max1ALT  13343  max0sub  13353  ifle  13354  xmulneg1  13426  fzprval  13746  fztpval  13747  modifeq2int  14103  seqf1olem1  14211  seqf1olem2  14212  bcval2  14476  tpf1ofv0  14668  tpf1ofv1  14669  ccatval1  14749  ccatalpha  14767  swrdccat  14912  pfxccat3a  14915  swrdccat3b  14917  repswswrd  14963  cshword  14970  0csh0  14972  ccatco  15014  sgnn  15276  max0add  15506  absmax  15526  sumrblem  15906  fsumcvg  15907  summolem2a  15910  isum  15914  sumss  15919  sumss2  15921  fsumcvg2  15922  fsumser  15925  fsumsplit  15936  sumsplit  15963  prodrblem  16125  fprodcvg  16126  prodmolem2a  16130  zprod  16133  iprod  16134  iprodn0  16136  prodss  16143  fprodsplit  16162  ruclem2  16429  ruclem3  16430  flodddiv4  16614  sadadd2lem2  16649  sadcf  16652  sadc0  16653  sadcp1  16654  sadcaddlem  16656  smupf  16677  smup0  16678  gcd0val  16696  dfgcd2  16748  eucalgf  16787  eucalginv  16788  eucalglt  16789  lcmf0val  16826  phisum  16997  pc0  17061  pcgcd  17085  pcmptcl  17098  pcmpt  17099  pcmpt2  17100  pcprod  17102  fldivp1  17104  prmreclem2  17124  prmreclem4  17126  1arithlem4  17133  vdwlem6  17193  ramtcl2  17218  ramcl2  17223  ramub1lem1  17233  prmop1  17245  fvprmselelfz  17251  fvprmselgcd1  17252  ressid2  17441  xpsfrnel  17763  xpsaddlem  17774  xpsvsca  17778  mreexexd  17851  gsumval1  18901  mgm2nsgrplem2  19147  sgrp2nmndlem2  19152  symgextfve  19663  symgfixfolem1  19682  pmtrmvd  19700  pmtrfinv  19705  pmtrprfval  19731  pmtrprfvalrn  19732  frgpuptinv  20015  frgpup2  20020  frgpup3lem  20021  cyggex  20142  gsumzsplit  20171  gsummpt1n0  20209  dprdfid  20263  dmdprdsplitlem  20283  sdrgacs  21088  abvtrivd  21119  znf1o  21887  uvcvv1  22125  psrlidm  22299  psrridm  22300  mvrf1  22323  mplmonmul  22375  mplcoe1  22376  mplcoe3  22377  mplcoe5  22379  mplmon2  22400  subrgasclcl  22406  evlslem3  22419  evlslem1  22421  selvvvval  22481  psdmul  22517  psdmvr  22520  coe1tmfv1  22623  ply1sclid  22637  dmatmul  22842  scmatscmiddistr  22853  1mavmul  22893  mulmarep1gsum2  22919  1marepvmarrepid  22920  mdetdiag  22944  mdetralt2  22954  mdetunilem2  22958  mdetunilem7  22963  mdetunilem8  22964  mdetunilem9  22965  mndifsplit  22981  maducoeval2  22985  madugsum  22988  madurid  22989  gsummatr01lem3  23002  gsummatr01  23004  smadiadetglem2  23017  matunitlindflem1  23024  1elcpmat  23063  decpmatid  23118  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  ptpjpre1  23920  ptbasfi  23930  ptpjopn  23961  isfcls  24358  ptcmplem2  24402  ptcmplem3  24403  tsmssplit  24501  dscmet  24921  dscopn  24922  icccmplem2  25173  iccpnfcnv  25295  xrhmeo  25297  pcopt  25373  pcopt2  25374  pcoass  25375  pcorevlem  25377  cmetcaulem  25639  ovolicc1  25867  ioorcl  25928  i1f1lem  26040  itg11  26042  itg1addlem2  26048  itg1addlem4  26050  i1fres  26056  itg1climres  26065  mbfi1fseqlem4  26069  mbfi1fseqlem5  26070  mbfi1flim  26074  itg2const2  26092  itg2seq  26093  itg2uba  26094  itg2splitlem  26099  itg2split  26100  itg2monolem1  26101  itg2cnlem1  26112  itg2cnlem2  26113  iblcnlem  26139  iblss  26155  iblss2  26156  itgitg2  26157  itgle  26160  itgss  26162  itgss2  26163  itgss3  26165  itgless  26167  ibladdlem  26170  itgaddlem1  26173  iblabslem  26178  iblabs  26179  iblabsr  26180  iblmulc2  26181  bddmulibl  26189  bddiblnc  26192  itggt0  26194  itgcn  26195  limcvallem  26221  ellimc2  26227  limccnp  26241  limccnp2  26242  limcco  26243  dvcobr  26296  dvexp2  26304  mon1pid  26502  elply2  26544  elplyd  26550  ply1termlem  26551  coe1termlem  26607  abelthlem9  26797  logtayl  27018  leibpilem2  27299  leibpi  27300  rlimcnp2  27324  efrlim  27327  igamz  27405  isnsqf  27492  mule1  27505  sqff1o  27539  muinv  27550  chtublem  27568  dchrelbasd  27596  bposlem1  27641  bposlem3  27643  bposlem5  27645  bposlem6  27646  lgsval2lem  27664  lgsneg  27678  lgsdilem  27681  lgsdir2  27687  lgsdir  27689  lgsdi  27691  lgsne0  27692  gausslemma2dlem1a  27722  2lgslem1c  27750  2lgslem3  27761  2lgs  27764  dchrvmasum2if  27854  dchrvmasumiflem1  27858  rpvmasum2  27869  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  padicabv  27987  ostth2lem4  27993  nosupno  28090  nosupbday  28092  nosupbnd1  28101  nosupbnd2  28103  noinfno  28105  noinfbday  28107  noinfbnd1  28116  maxs1  28156  maxs2  28157  mins1  28158  mins2  28159  abssid  28657  abssge0  28661  axlowdimlem15  29564  opvtxval  29611  opiedgval  29614  elimifd  33211  elim2if  33212  ifeq3da  33214  ifnefals  33216  fmptunsnop  33364  pmtridf1o  33725  fzto1stfv1  33732  resvid2  33961  psrmonmul  34252  vieta  34282  2sqr3minply  34482  cos9thpiminply  34490  xrge0iifcnv  34635  xrge0iifiso  34637  xrge0iifhom  34639  sigaclfu2  34823  ddeval1  34937  eulerpartlemb  35070  ballotlemsima  35218  ballotlemrv1  35223  signsw0glem  35252  signswmnd  35256  signswrid  35257  jaeqifi  35782  ordunmax  35792  soinfdom  35800  vonf1oonfo  36049  onf1oracwevd  36052  onprcf1of1ord  36055  indispconn  36166  ex-sategoelel  36353  ex-sategoelelomsuc  36358  ex-sategoelel12  36359  mrsubvr  36443  dfrdg2  36735  dfrdg3  36736  unisnif  36865  dfrdg4  36893  fnejoin2  37335  unbdqndv2lem2  37554  bj-xpima2sn  38049  finxpreclem1  38504  finxpreclem3  38508  poimirlem2  38732  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem24  38754  mblfinlem2  38768  mbfposadd  38777  itg2addnclem  38781  itg2gt0cn  38785  ibladdnclem  38786  itgaddnclem1  38788  iblabsnclem  38793  iblabsnc  38794  iblmulc2nc  38795  itggt0cn  38800  ftc1anclem4  38806  ftc1anclem5  38807  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  areacirclem5  38822  areacirc  38823  fdc  38871  heiborlem4  38940  ac6s6  39296  cdleme27a  41616  cdleme31sn1  41630  cdleme31fv1  41640  cdlemk40t  42167  dihvalb  42486  sticksstones12a  43399  brif2  43471  brif12  43472  evlsbagval  43807  fsuppind  43811  dffltz  43863  pw2f1ocnv  44237  aomclem5  44253  kelac1  44258  arearect  44409  areaquad  44410  oe0rif  44479  cantnfresb  44518  safesnsupfidom1o  44610  safesnsupfilb  44611  clsk1indlem1  45237  refsum2cnlem1  46259  upbdrech2  46529  lptioo2  46848  lptioo1  46849  limsupmnfuzlem  46941  limsupre3uzlem  46950  limsup10exlem  46987  coskpi2  47081  cosknegpi  47084  cncfiooicclem1  47108  cncfiooiccre  47110  dvnxpaek  47157  dvnprodlem1  47161  dvnprodlem3  47163  itgioocnicc  47192  iblcncfioo  47193  volico  47198  sublevolico  47199  volioore  47205  voliooico  47207  voliccico  47214  dirkerper  47311  dirkertrigeq  47316  dirkercncflem2  47319  fourierdlem10  47332  fourierdlem32  47354  fourierdlem33  47355  fourierdlem37  47359  fourierdlem62  47383  fourierdlem73  47394  fourierdlem74  47395  fourierdlem75  47396  fourierdlem79  47400  fourierdlem81  47402  fourierdlem82  47403  fourierdlem93  47414  fourierdlem97  47418  fourierdlem101  47422  fourierdlem103  47424  fourierdlem104  47425  sqwvfoura  47443  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  etransclem4  47453  etransclem15  47464  etransclem19  47468  etransclem20  47469  etransclem23  47472  etransclem24  47473  etransclem25  47474  etransclem27  47476  etransclem31  47480  etransclem32  47481  ioorrnopnxrlem  47521  nnfoctbdjlem  47670  isomenndlem  47745  ovn0val  47765  hoidmv0val  47798  hsphoidmvle2  47800  hoidmv1lelem1  47806  hoidmv1lelem2  47807  hoidmv1le  47809  hoidmvlelem2  47811  hoidmvlelem3  47812  ovnhoilem1  47816  hspdifhsp  47831  hoidifhspdmvle  47835  hspmbllem1  47841  hspmbllem2  47842  hspmbl  47844  volico2  47856  ovnsubadd2lem  47860  ovolval4lem2  47865  ovolval5lem1  47867  aiotaexim  48373  afvfundmfveq  48413  dfatafv2iota  48485  dfatafv2eqfv  48536  difmodm1lt  48640  prproropf1olem3  48792  prproropf1olem4  48793  linc1  49742  lincext3  49773  lindslinindsimp1  49774  el0ldep  49783  islindeps2  49800  itcoval0  49979  ackval0  49997  crosspv1d  51240  crosspv2d  51241  veronesev1lem  51253  veronesev2lem  51254  veronesev3lem  51255  veronesev4lem  51256  veronesev5lem  51257  veronesev6lem  51258  veronesevrowd  51259