Theorem iftrue 4554

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 4550	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1044	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	eqabdv 2878	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2799	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {cab 2717  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  iftruei  4555  iftrued  4556  ifsb  4561  ifbi  4570  ifeq2da  4580  ifeq12da  4581  ifclda  4583  ifeqda  4584  elimif  4585  ifbothda  4586  ifid  4588  ifeqor  4599  ifnot  4600  ifan  4601  ifor  4602  2if2  4603  dedth  4606  elimhyp  4613  elimhyp2v  4614  elimhyp3v  4615  elimhyp4v  4616  elimdhyp  4618  keephyp2v  4620  keephyp3v  4621  dfopif  4894  dfopg  4895  somin1  6165  somincom  6166  xpima1  6214  elimdelov  7546  brif1  7547  ovif12  7550  tz7.44-1  8462  rdg0n  8490  resixpfo  8994  boxriin  8998  boxcutc  8999  pw2f1olem  9142  unxpdomlem2  9314  unxpdomlem3  9315  infsupprpr  9573  ordtypelem1  9587  wemaplem2  9616  unwdomg  9653  ixpiunwdom  9659  cantnfp1lem2  9748  cantnfp1lem3  9749  ssttrcl  9784  ttrclselem2  9795  acndom  10120  dfac12lem2  10214  fin23lem14  10402  axcc2lem  10505  pwfseqlem2  10728  uzin  12943  xrmax1  13237  xrmax2  13238  xrmin1  13239  xrmin2  13240  max1ALT  13248  max0sub  13258  ifle  13259  xmulneg1  13331  fzprval  13645  fztpval  13646  modifeq2int  13984  seqf1olem1  14092  seqf1olem2  14093  bcval2  14354  tpf1ofv0  14545  tpf1ofv1  14546  ccatval1  14625  ccatalpha  14641  swrdccat  14783  pfxccat3a  14786  swrdccat3b  14788  repswswrd  14832  cshword  14839  0csh0  14841  ccatco  14884  sgnn  15143  max0add  15359  absmax  15378  sumrblem  15759  fsumcvg  15760  summolem2a  15763  isum  15767  sumss  15772  sumss2  15774  fsumcvg2  15775  fsumser  15778  fsumsplit  15789  sumsplit  15816  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  zprod  15985  iprod  15986  iprodn0  15988  prodss  15995  fprodsplit  16014  ruclem2  16280  ruclem3  16281  flodddiv4  16461  sadadd2lem2  16496  sadcf  16499  sadc0  16500  sadcp1  16501  sadcaddlem  16503  smupf  16524  smup0  16525  gcd0val  16543  dfgcd2  16593  eucalgf  16630  eucalginv  16631  eucalglt  16632  lcmf0val  16669  phisum  16837  pc0  16901  pcgcd  16925  pcmptcl  16938  pcmpt  16939  pcmpt2  16940  pcprod  16942  fldivp1  16944  prmreclem2  16964  prmreclem4  16966  1arithlem4  16973  vdwlem6  17033  ramtcl2  17058  ramcl2  17063  ramub1lem1  17073  prmop1  17085  fvprmselelfz  17091  fvprmselgcd1  17092  ressid2  17291  xpsfrnel  17622  xpsaddlem  17633  xpsvsca  17637  mreexexd  17706  gsumval1  18721  mgm2nsgrplem2  18954  sgrp2nmndlem2  18959  symgextfve  19461  symgfixfolem1  19480  pmtrmvd  19498  pmtrfinv  19503  pmtrprfval  19529  pmtrprfvalrn  19530  frgpuptinv  19813  frgpup2  19818  frgpup3lem  19819  cyggex  19940  gsumzsplit  19969  gsummpt1n0  20007  dprdfid  20061  dmdprdsplitlem  20081  sdrgacs  20824  abvtrivd  20855  znf1o  21593  uvcvv1  21832  psrlidm  22005  psrridm  22006  mvrf1  22029  mplmonmul  22077  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  mplmon2  22108  subrgasclcl  22114  evlslem3  22127  evlslem1  22129  psdmul  22193  coe1tmfv1  22298  ply1sclid  22312  dmatmul  22524  scmatscmiddistr  22535  1mavmul  22575  mulmarep1gsum2  22601  1marepvmarrepid  22602  mdetdiag  22626  mdetralt2  22636  mdetunilem2  22640  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  mndifsplit  22663  maducoeval2  22667  madugsum  22670  madurid  22671  gsummatr01lem3  22684  gsummatr01  22686  smadiadetglem2  22699  1elcpmat  22742  decpmatid  22797  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  ptpjpre1  23600  ptbasfi  23610  ptpjopn  23641  isfcls  24038  ptcmplem2  24082  ptcmplem3  24083  tsmssplit  24181  dscmet  24606  dscopn  24607  icccmplem2  24864  iccpnfcnv  24994  xrhmeo  24996  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  cmetcaulem  25341  ovolicc1  25570  ioorcl  25631  i1f1lem  25743  itg11  25745  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1flim  25778  itg2const2  25796  itg2seq  25797  itg2uba  25798  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2cnlem1  25816  itg2cnlem2  25817  iblcnlem  25844  iblss  25860  iblss2  25861  itgitg2  25862  itgle  25865  itgss  25867  itgss2  25868  itgss3  25870  itgless  25872  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  iblabs  25884  iblabsr  25885  iblmulc2  25886  bddmulibl  25894  bddiblnc  25897  itggt0  25899  itgcn  25900  limcvallem  25926  ellimc2  25932  limccnp  25946  limccnp2  25947  limcco  25948  dvcobr  26003  dvcobrOLD  26004  dvexp2  26012  mon1pid  26213  elply2  26255  elplyd  26261  ply1termlem  26262  coe1termlem  26317  abelthlem9  26502  logtayl  26720  leibpilem2  27002  leibpi  27003  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  igamz  27109  isnsqf  27196  mule1  27209  sqff1o  27243  muinv  27254  chtublem  27273  dchrelbasd  27301  bposlem1  27346  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgsval2lem  27369  lgsneg  27383  lgsdilem  27386  lgsdir2  27392  lgsdir  27394  lgsdi  27396  lgsne0  27397  gausslemma2dlem1a  27427  2lgslem1c  27455  2lgslem3  27466  2lgs  27469  dchrvmasum2if  27559  dchrvmasumiflem1  27563  rpvmasum2  27574  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  padicabv  27692  ostth2lem4  27698  nosupno  27766  nosupbday  27768  nosupbnd1  27777  nosupbnd2  27779  noinfno  27781  noinfbday  27783  noinfbnd1  27792  maxs1  27828  maxs2  27829  mins1  27830  mins2  27831  abssid  28283  abssge0  28287  axlowdimlem15  28989  opvtxval  29038  opiedgval  29041  elimifd  32566  elim2if  32567  ifeq3da  32569  ifnefals  32571  pmtridf1o  33087  fzto1stfv1  33094  resvid2  33319  2sqr3minply  33738  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  indval2  33978  ind1  33981  sigaclfu2  34085  ddeval1  34198  eulerpartlemb  34333  ballotlemsima  34480  ballotlemrv1  34485  signsw0glem  34530  signswmnd  34534  signswrid  34535  indispconn  35202  ex-sategoelel  35389  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  mrsubvr  35479  dfrdg2  35759  dfrdg3  35760  unisnif  35889  dfrdg4  35915  fnejoin2  36335  unbdqndv2lem2  36476  bj-xpima2sn  36924  finxpreclem1  37355  finxpreclem3  37359  matunitlindflem1  37576  poimirlem2  37582  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  mblfinlem2  37618  mbfposadd  37627  itg2addnclem  37631  itg2gt0cn  37635  ibladdnclem  37636  itgaddnclem1  37638  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  itggt0cn  37650  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirclem5  37672  areacirc  37673  fdc  37705  heiborlem4  37774  ac6s6  38132  cdleme27a  40324  cdleme31sn1  40338  cdleme31fv1  40348  cdlemk40t  40875  dihvalb  41194  sticksstones12a  42114  metakunt5  42166  metakunt6  42167  metakunt10  42171  metakunt11  42172  metakunt20  42181  brif2  42217  brif12  42218  evlsbagval  42521  selvvvval  42540  fsuppind  42545  dffltz  42589  pw2f1ocnv  42994  aomclem5  43015  kelac1  43020  arearect  43176  areaquad  43177  oe0rif  43247  cantnfresb  43286  safesnsupfidom1o  43379  safesnsupfilb  43380  clsk1indlem1  44007  refsum2cnlem1  44937  upbdrech2  45223  lptioo2  45552  lptioo1  45553  limsupmnfuzlem  45647  limsupre3uzlem  45656  limsup10exlem  45693  coskpi2  45787  cosknegpi  45790  cncfiooicclem1  45814  cncfiooiccre  45816  dvnxpaek  45863  dvnprodlem1  45867  dvnprodlem3  45869  itgioocnicc  45898  iblcncfioo  45899  volico  45904  sublevolico  45905  volioore  45911  voliooico  45913  voliccico  45920  dirkerper  46017  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem10  46038  fourierdlem32  46060  fourierdlem33  46061  fourierdlem37  46065  fourierdlem62  46089  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem93  46120  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem4  46159  etransclem15  46170  etransclem19  46174  etransclem20  46175  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem27  46182  etransclem31  46186  etransclem32  46187  ioorrnopnxrlem  46227  nnfoctbdjlem  46376  isomenndlem  46451  ovn0val  46471  hoidmv0val  46504  hsphoidmvle2  46506  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  hspdifhsp  46537  hoidifhspdmvle  46541  hspmbllem1  46547  hspmbllem2  46548  hspmbl  46550  volico2  46562  ovnsubadd2lem  46566  ovolval4lem2  46571  ovolval5lem1  46573  afvfundmfveq  47053  dfatafv2iota  47125  dfatafv2eqfv  47176  prproropf1olem3  47379  prproropf1olem4  47380  linc1  48154  lincext3  48185  lindslinindsimp1  48186  el0ldep  48195  islindeps2  48212  itcoval0  48396  ackval0  48414