Theorem iftrue 4492

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2141  {cab 2739  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487

This theorem is referenced by:  iftruei  4493  iftrued  4494  iftrueb  4499  ifsb  4500  ifbi  4509  ifeq2da  4519  ifeq12da  4520  ifclda  4522  ifeqda  4523  elimif  4524  ifbothda  4525  ifid  4527  ifeqor  4538  ifnot  4539  ifan  4540  ifor  4541  2if2  4542  dedth  4545  elimhyp  4552  elimhyp2v  4553  elimhyp3v  4554  elimhyp4v  4555  elimdhyp  4557  keephyp2v  4559  keephyp3v  4560  dfopif  4834  dfopg  4835  somin1  6133  somincom  6134  xpima1  6181  elimdelov  7506  brif1  7507  ovif12  7510  ifmpt2v  7512  tz7.44-1  8392  rdg0n  8420  resixpfo  8933  boxriin  8937  boxcutc  8938  pw2f1olem  9068  unxpdomlem2  9216  unxpdomlem3  9217  infsupprpr  9465  ordtypelem1  9479  wemaplem2  9508  unwdomg  9545  ixpiunwdom  9551  cantnfp1lem2  9647  cantnfp1lem3  9648  ssttrcl  9683  ttrclselem2  9694  acndom  10034  dfac12lem2  10127  fin23lem14  10316  axcc2lem  10419  pwfseqlem2  10643  indval2  12222  ind1  12226  uzin  12897  xrmax1  13200  xrmax2  13201  xrmin1  13202  xrmin2  13203  max1ALT  13211  max0sub  13221  ifle  13222  xmulneg1  13294  fzprval  13613  fztpval  13614  modifeq2int  13969  seqf1olem1  14077  seqf1olem2  14078  bcval2  14341  tpf1ofv0  14533  tpf1ofv1  14534  ccatval1  14614  ccatalpha  14631  swrdccat  14772  pfxccat3a  14775  swrdccat3b  14777  repswswrd  14821  cshword  14828  0csh0  14830  ccatco  14872  sgnn  15131  max0add  15361  absmax  15381  sumrblem  15762  fsumcvg  15763  summolem2a  15766  isum  15770  sumss  15775  sumss2  15777  fsumcvg2  15778  fsumser  15781  fsumsplit  15792  sumsplit  15819  prodrblem  15983  fprodcvg  15984  prodmolem2a  15988  zprod  15991  iprod  15992  iprodn0  15994  prodss  16001  fprodsplit  16020  ruclem2  16287  ruclem3  16288  flodddiv4  16472  sadadd2lem2  16507  sadcf  16510  sadc0  16511  sadcp1  16512  sadcaddlem  16514  smupf  16535  smup0  16536  gcd0val  16554  dfgcd2  16603  eucalgf  16640  eucalginv  16641  eucalglt  16642  lcmf0val  16679  phisum  16849  pc0  16913  pcgcd  16937  pcmptcl  16950  pcmpt  16951  pcmpt2  16952  pcprod  16954  fldivp1  16956  prmreclem2  16976  prmreclem4  16978  1arithlem4  16985  vdwlem6  17045  ramtcl2  17070  ramcl2  17075  ramub1lem1  17085  prmop1  17097  fvprmselelfz  17103  fvprmselgcd1  17104  ressid2  17293  xpsfrnel  17615  xpsaddlem  17626  xpsvsca  17630  mreexexd  17703  gsumval1  18740  mgm2nsgrplem2  18980  sgrp2nmndlem2  18985  symgextfve  19488  symgfixfolem1  19507  pmtrmvd  19525  pmtrfinv  19530  pmtrprfval  19556  pmtrprfvalrn  19557  frgpuptinv  19840  frgpup2  19845  frgpup3lem  19846  cyggex  19967  gsumzsplit  19996  gsummpt1n0  20034  dprdfid  20088  dmdprdsplitlem  20108  sdrgacs  20883  abvtrivd  20914  znf1o  21680  uvcvv1  21918  psrlidm  22090  psrridm  22091  mvrf1  22114  mplmonmul  22166  mplcoe1  22167  mplcoe3  22168  mplcoe5  22170  mplmon2  22191  subrgasclcl  22197  evlslem3  22210  evlslem1  22212  selvvvval  22272  psdmul  22308  psdmvr  22311  coe1tmfv1  22414  ply1sclid  22428  dmatmul  22633  scmatscmiddistr  22644  1mavmul  22684  mulmarep1gsum2  22710  1marepvmarrepid  22711  mdetdiag  22735  mdetralt2  22745  mdetunilem2  22749  mdetunilem7  22754  mdetunilem8  22755  mdetunilem9  22756  mndifsplit  22772  maducoeval2  22776  madugsum  22779  madurid  22780  gsummatr01lem3  22793  gsummatr01  22795  smadiadetglem2  22808  1elcpmat  22851  decpmatid  22906  chfacfscmulgsum  22996  chfacfpmmulgsum  23000  ptpjpre1  23707  ptbasfi  23717  ptpjopn  23748  isfcls  24145  ptcmplem2  24189  ptcmplem3  24190  tsmssplit  24288  dscmet  24708  dscopn  24709  icccmplem2  24960  iccpnfcnv  25082  xrhmeo  25084  pcopt  25160  pcopt2  25161  pcoass  25162  pcorevlem  25164  cmetcaulem  25426  ovolicc1  25654  ioorcl  25715  i1f1lem  25827  itg11  25829  itg1addlem2  25835  itg1addlem4  25837  i1fres  25843  itg1climres  25852  mbfi1fseqlem4  25856  mbfi1fseqlem5  25857  mbfi1flim  25861  itg2const2  25879  itg2seq  25880  itg2uba  25881  itg2splitlem  25886  itg2split  25887  itg2monolem1  25888  itg2cnlem1  25899  itg2cnlem2  25900  iblcnlem  25927  iblss  25943  iblss2  25944  itgitg2  25945  itgle  25948  itgss  25950  itgss2  25951  itgss3  25953  itgless  25955  ibladdlem  25958  itgaddlem1  25961  iblabslem  25966  iblabs  25967  iblabsr  25968  iblmulc2  25969  bddmulibl  25977  bddiblnc  25980  itggt0  25982  itgcn  25983  limcvallem  26009  ellimc2  26015  limccnp  26029  limccnp2  26030  limcco  26031  dvcobr  26084  dvexp2  26092  mon1pid  26290  elply2  26332  elplyd  26338  ply1termlem  26339  coe1termlem  26394  abelthlem9  26579  logtayl  26801  leibpilem2  27082  leibpi  27083  rlimcnp2  27107  efrlim  27110  igamz  27188  isnsqf  27275  mule1  27288  sqff1o  27322  muinv  27333  chtublem  27351  dchrelbasd  27379  bposlem1  27424  bposlem3  27426  bposlem5  27428  bposlem6  27429  lgsval2lem  27447  lgsneg  27461  lgsdilem  27464  lgsdir2  27470  lgsdir  27472  lgsdi  27474  lgsne0  27475  gausslemma2dlem1a  27505  2lgslem1c  27533  2lgslem3  27544  2lgs  27547  dchrvmasum2if  27637  dchrvmasumiflem1  27641  rpvmasum2  27652  pntrlog2bndlem4  27720  pntrlog2bndlem5  27721  padicabv  27770  ostth2lem4  27776  nosupno  27843  nosupbday  27845  nosupbnd1  27854  nosupbnd2  27856  noinfno  27858  noinfbday  27860  noinfbnd1  27869  maxs1  27909  maxs2  27910  mins1  27911  mins2  27912  abssid  28410  abssge0  28414  axlowdimlem15  29272  opvtxval  29319  opiedgval  29322  elimifd  32855  elim2if  32856  ifeq3da  32858  ifnefals  32860  fmptunsnop  33011  pmtridf1o  33380  fzto1stfv1  33387  resvid2  33616  psrmonmul  33906  vieta  33936  2sqr3minply  34136  cos9thpiminply  34144  xrge0iifcnv  34289  xrge0iifiso  34291  xrge0iifhom  34293  sigaclfu2  34477  ddeval1  34590  eulerpartlemb  34724  ballotlemsima  34872  ballotlemrv1  34877  signsw0glem  34906  signswmnd  34910  signswrid  34911  vonf1oonfo  35565  indispconn  35692  ex-sategoelel  35879  ex-sategoelelomsuc  35884  ex-sategoelel12  35885  mrsubvr  35969  dfrdg2  36251  dfrdg3  36252  unisnif  36381  dfrdg4  36409  fnejoin2  36846  unbdqndv2lem2  37065  bj-xpima2sn  37560  finxpreclem1  38001  finxpreclem3  38005  matunitlindflem1  38233  poimirlem2  38239  poimirlem15  38252  poimirlem16  38253  poimirlem17  38254  poimirlem19  38256  poimirlem20  38257  poimirlem24  38261  mblfinlem2  38275  mbfposadd  38284  itg2addnclem  38288  itg2gt0cn  38292  ibladdnclem  38293  itgaddnclem1  38295  iblabsnclem  38300  iblabsnc  38301  iblmulc2nc  38302  itggt0cn  38307  ftc1anclem4  38313  ftc1anclem5  38314  ftc1anclem6  38315  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318  areacirclem5  38329  areacirc  38330  fdc  38362  heiborlem4  38431  ac6s6  38789  cdleme27a  41109  cdleme31sn1  41123  cdleme31fv1  41133  cdlemk40t  41660  dihvalb  41979  sticksstones12a  42892  brif2  42963  brif12  42964  evlsbagval  43288  fsuppind  43292  dffltz  43336  pw2f1ocnv  43734  aomclem5  43755  kelac1  43760  arearect  43912  areaquad  43913  oe0rif  43982  cantnfresb  44021  safesnsupfidom1o  44113  safesnsupfilb  44114  clsk1indlem1  44741  refsum2cnlem1  45727  upbdrech2  45997  lptioo2  46317  lptioo1  46318  limsupmnfuzlem  46410  limsupre3uzlem  46419  limsup10exlem  46456  coskpi2  46550  cosknegpi  46553  cncfiooicclem1  46577  cncfiooiccre  46579  dvnxpaek  46626  dvnprodlem1  46630  dvnprodlem3  46632  itgioocnicc  46661  iblcncfioo  46662  volico  46667  sublevolico  46668  volioore  46674  voliooico  46676  voliccico  46683  dirkerper  46780  dirkertrigeq  46785  dirkercncflem2  46788  fourierdlem10  46801  fourierdlem32  46823  fourierdlem33  46824  fourierdlem37  46828  fourierdlem62  46852  fourierdlem73  46863  fourierdlem74  46864  fourierdlem75  46865  fourierdlem79  46869  fourierdlem81  46871  fourierdlem82  46872  fourierdlem93  46883  fourierdlem97  46887  fourierdlem101  46891  fourierdlem103  46893  fourierdlem104  46894  sqwvfoura  46912  sqwvfourb  46913  fourierswlem  46914  fouriersw  46915  etransclem4  46922  etransclem15  46933  etransclem19  46937  etransclem20  46938  etransclem23  46941  etransclem24  46942  etransclem25  46943  etransclem27  46945  etransclem31  46949  etransclem32  46950  ioorrnopnxrlem  46990  nnfoctbdjlem  47139  isomenndlem  47214  ovn0val  47234  hoidmv0val  47267  hsphoidmvle2  47269  hoidmv1lelem1  47275  hoidmv1lelem2  47276  hoidmv1le  47278  hoidmvlelem2  47280  hoidmvlelem3  47281  ovnhoilem1  47285  hspdifhsp  47300  hoidifhspdmvle  47304  hspmbllem1  47310  hspmbllem2  47311  hspmbl  47313  volico2  47325  ovnsubadd2lem  47329  ovolval4lem2  47334  ovolval5lem1  47336  afvfundmfveq  47842  dfatafv2iota  47914  dfatafv2eqfv  47965  difmodm1lt  48069  prproropf1olem3  48221  prproropf1olem4  48222  linc1  49172  lincext3  49203  lindslinindsimp1  49204  el0ldep  49213  islindeps2  49230  itcoval0  49409  ackval0  49427