Theorem iftrue 4489

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {cab 2743  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  iftruei  4490  iftrued  4491  iftrueb  4496  ifsb  4497  ifbi  4506  ifeq2da  4516  ifeq12da  4517  ifclda  4519  ifeqda  4520  elimif  4521  ifbothda  4522  ifid  4524  ifeqor  4535  ifnot  4536  ifan  4537  ifor  4538  2if2  4539  dedth  4542  elimhyp  4549  elimhyp2v  4550  elimhyp3v  4551  elimhyp4v  4552  elimdhyp  4554  keephyp2v  4556  keephyp3v  4557  dfopif  4831  dfopg  4832  somin1  6124  somincom  6125  xpima1  6173  elimdelov  7496  brif1  7497  ovif12  7500  ifmpt2v  7502  tz7.44-1  8381  rdg0n  8409  resixpfo  8922  boxriin  8926  boxcutc  8927  pw2f1olem  9057  unxpdomlem2  9205  unxpdomlem3  9206  infsupprpr  9454  ordtypelem1  9468  wemaplem2  9497  unwdomg  9534  ixpiunwdom  9540  cantnfp1lem2  9636  cantnfp1lem3  9637  ssttrcl  9672  ttrclselem2  9683  acndom  10023  dfac12lem2  10116  fin23lem14  10305  axcc2lem  10408  pwfseqlem2  10632  indval2  12214  ind1  12218  uzin  12889  xrmax1  13192  xrmax2  13193  xrmin1  13194  xrmin2  13195  max1ALT  13203  max0sub  13213  ifle  13214  xmulneg1  13286  fzprval  13604  fztpval  13605  modifeq2int  13960  seqf1olem1  14068  seqf1olem2  14069  bcval2  14332  tpf1ofv0  14523  tpf1ofv1  14524  ccatval1  14604  ccatalpha  14621  swrdccat  14762  pfxccat3a  14765  swrdccat3b  14767  repswswrd  14811  cshword  14818  0csh0  14820  ccatco  14862  sgnn  15121  max0add  15351  absmax  15371  sumrblem  15752  fsumcvg  15753  summolem2a  15756  isum  15760  sumss  15765  sumss2  15767  fsumcvg2  15768  fsumser  15771  fsumsplit  15782  sumsplit  15809  prodrblem  15973  fprodcvg  15974  prodmolem2a  15978  zprod  15981  iprod  15982  iprodn0  15984  prodss  15991  fprodsplit  16010  ruclem2  16278  ruclem3  16279  flodddiv4  16463  sadadd2lem2  16498  sadcf  16501  sadc0  16502  sadcp1  16503  sadcaddlem  16505  smupf  16526  smup0  16527  gcd0val  16545  dfgcd2  16594  eucalgf  16631  eucalginv  16632  eucalglt  16633  lcmf0val  16670  phisum  16840  pc0  16904  pcgcd  16928  pcmptcl  16941  pcmpt  16942  pcmpt2  16943  pcprod  16945  fldivp1  16947  prmreclem2  16967  prmreclem4  16969  1arithlem4  16976  vdwlem6  17036  ramtcl2  17061  ramcl2  17066  ramub1lem1  17076  prmop1  17088  fvprmselelfz  17094  fvprmselgcd1  17095  ressid2  17284  xpsfrnel  17606  xpsaddlem  17617  xpsvsca  17621  mreexexd  17694  gsumval1  18731  mgm2nsgrplem2  18971  sgrp2nmndlem2  18976  symgextfve  19480  symgfixfolem1  19499  pmtrmvd  19517  pmtrfinv  19522  pmtrprfval  19548  pmtrprfvalrn  19549  frgpuptinv  19832  frgpup2  19837  frgpup3lem  19838  cyggex  19959  gsumzsplit  19988  gsummpt1n0  20026  dprdfid  20080  dmdprdsplitlem  20100  sdrgacs  20873  abvtrivd  20904  znf1o  21661  uvcvv1  21899  psrlidm  22071  psrridm  22072  mvrf1  22095  mplmonmul  22147  mplcoe1  22148  mplcoe3  22149  mplcoe5  22151  mplmon2  22172  subrgasclcl  22178  evlslem3  22191  evlslem1  22193  selvvvval  22253  psdmul  22289  psdmvr  22292  coe1tmfv1  22395  ply1sclid  22409  dmatmul  22615  scmatscmiddistr  22626  1mavmul  22666  mulmarep1gsum2  22692  1marepvmarrepid  22693  mdetdiag  22717  mdetralt2  22727  mdetunilem2  22731  mdetunilem7  22736  mdetunilem8  22737  mdetunilem9  22738  mndifsplit  22754  maducoeval2  22758  madugsum  22761  madurid  22762  gsummatr01lem3  22775  gsummatr01  22777  smadiadetglem2  22790  1elcpmat  22833  decpmatid  22888  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  ptpjpre1  23689  ptbasfi  23699  ptpjopn  23730  isfcls  24127  ptcmplem2  24171  ptcmplem3  24172  tsmssplit  24270  dscmet  24690  dscopn  24691  icccmplem2  24942  iccpnfcnv  25064  xrhmeo  25066  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  cmetcaulem  25408  ovolicc1  25636  ioorcl  25697  i1f1lem  25809  itg11  25811  itg1addlem2  25817  itg1addlem4  25819  i1fres  25825  itg1climres  25834  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1flim  25843  itg2const2  25861  itg2seq  25862  itg2uba  25863  itg2splitlem  25868  itg2split  25869  itg2monolem1  25870  itg2cnlem1  25881  itg2cnlem2  25882  iblcnlem  25909  iblss  25925  iblss2  25926  itgitg2  25927  itgle  25930  itgss  25932  itgss2  25933  itgss3  25935  itgless  25937  ibladdlem  25940  itgaddlem1  25943  iblabslem  25948  iblabs  25949  iblabsr  25950  iblmulc2  25951  bddmulibl  25959  bddiblnc  25962  itggt0  25964  itgcn  25965  limcvallem  25991  ellimc2  25997  limccnp  26011  limccnp2  26012  limcco  26013  dvcobr  26066  dvexp2  26074  mon1pid  26272  elply2  26314  elplyd  26320  ply1termlem  26321  coe1termlem  26376  abelthlem9  26561  logtayl  26783  leibpilem2  27064  leibpi  27065  rlimcnp2  27089  efrlim  27092  igamz  27170  isnsqf  27257  mule1  27270  sqff1o  27304  muinv  27315  chtublem  27333  dchrelbasd  27361  bposlem1  27406  bposlem3  27408  bposlem5  27410  bposlem6  27411  lgsval2lem  27429  lgsneg  27443  lgsdilem  27446  lgsdir2  27452  lgsdir  27454  lgsdi  27456  lgsne0  27457  gausslemma2dlem1a  27487  2lgslem1c  27515  2lgslem3  27526  2lgs  27529  dchrvmasum2if  27619  dchrvmasumiflem1  27623  rpvmasum2  27634  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  padicabv  27752  ostth2lem4  27758  nosupno  27825  nosupbday  27827  nosupbnd1  27836  nosupbnd2  27838  noinfno  27840  noinfbday  27842  noinfbnd1  27851  maxs1  27891  maxs2  27892  mins1  27893  mins2  27894  abssid  28392  abssge0  28396  axlowdimlem15  29215  opvtxval  29262  opiedgval  29265  elimifd  32799  elim2if  32800  ifeq3da  32802  ifnefals  32804  fmptunsnop  32957  pmtridf1o  33327  fzto1stfv1  33334  resvid2  33565  psrmonmul  33857  vieta  33887  2sqr3minply  34087  cos9thpiminply  34095  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  sigaclfu2  34428  ddeval1  34541  eulerpartlemb  34675  ballotlemsima  34823  ballotlemrv1  34828  signsw0glem  34857  signswmnd  34861  signswrid  34862  vonf1oonfo  35470  indispconn  35597  ex-sategoelel  35784  ex-sategoelelomsuc  35789  ex-sategoelel12  35790  mrsubvr  35874  dfrdg2  36156  dfrdg3  36157  unisnif  36286  dfrdg4  36314  fnejoin2  36742  unbdqndv2lem2  36961  bj-xpima2sn  37455  finxpreclem1  37895  finxpreclem3  37899  matunitlindflem1  38127  poimirlem2  38133  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem24  38155  mblfinlem2  38169  mbfposadd  38178  itg2addnclem  38182  itg2gt0cn  38186  ibladdnclem  38187  itgaddnclem1  38189  iblabsnclem  38194  iblabsnc  38195  iblmulc2nc  38196  itggt0cn  38201  ftc1anclem4  38207  ftc1anclem5  38208  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  areacirclem5  38223  areacirc  38224  fdc  38256  heiborlem4  38325  ac6s6  38683  cdleme27a  41003  cdleme31sn1  41017  cdleme31fv1  41027  cdlemk40t  41554  dihvalb  41873  sticksstones12a  42786  brif2  42855  brif12  42856  evlsbagval  43180  fsuppind  43184  dffltz  43228  pw2f1ocnv  43626  aomclem5  43647  kelac1  43652  arearect  43804  areaquad  43805  oe0rif  43874  cantnfresb  43913  safesnsupfidom1o  44005  safesnsupfilb  44006  clsk1indlem1  44633  refsum2cnlem1  45615  upbdrech2  45885  lptioo2  46205  lptioo1  46206  limsupmnfuzlem  46298  limsupre3uzlem  46307  limsup10exlem  46344  coskpi2  46438  cosknegpi  46441  cncfiooicclem1  46465  cncfiooiccre  46467  dvnxpaek  46514  dvnprodlem1  46518  dvnprodlem3  46520  itgioocnicc  46549  iblcncfioo  46550  volico  46555  sublevolico  46556  volioore  46562  voliooico  46564  voliccico  46571  dirkerper  46668  dirkertrigeq  46673  dirkercncflem2  46676  fourierdlem10  46689  fourierdlem32  46711  fourierdlem33  46712  fourierdlem37  46716  fourierdlem62  46740  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem79  46757  fourierdlem81  46759  fourierdlem82  46760  fourierdlem93  46771  fourierdlem97  46775  fourierdlem101  46779  fourierdlem103  46781  fourierdlem104  46782  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  etransclem4  46810  etransclem15  46821  etransclem19  46825  etransclem20  46826  etransclem23  46829  etransclem24  46830  etransclem25  46831  etransclem27  46833  etransclem31  46837  etransclem32  46838  ioorrnopnxrlem  46878  nnfoctbdjlem  47027  isomenndlem  47102  ovn0val  47122  hoidmv0val  47155  hsphoidmvle2  47157  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmv1le  47166  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoilem1  47173  hspdifhsp  47188  hoidifhspdmvle  47192  hspmbllem1  47198  hspmbllem2  47199  hspmbl  47201  volico2  47213  ovnsubadd2lem  47217  ovolval4lem2  47222  ovolval5lem1  47224  afvfundmfveq  47730  dfatafv2iota  47802  dfatafv2eqfv  47853  difmodm1lt  47957  prproropf1olem3  48109  prproropf1olem4  48110  linc1  49056  lincext3  49087  lindslinindsimp1  49088  el0ldep  49097  islindeps2  49114  itcoval0  49293  ackval0  49311