Theorem iftrue 4534

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  iftruei  4535  iftrued  4536  ifsb  4541  ifbi  4550  ifeq2da  4560  ifeq12da  4561  ifclda  4563  ifeqda  4564  elimif  4565  ifbothda  4566  ifid  4568  ifeqor  4579  ifnot  4580  ifan  4581  ifor  4582  2if2  4583  dedth  4586  elimhyp  4593  elimhyp2v  4594  elimhyp3v  4595  elimhyp4v  4596  elimdhyp  4598  keephyp2v  4600  keephyp3v  4601  dfopif  4870  dfopg  4871  somin1  6132  somincom  6133  xpima1  6180  elimdelov  7502  ovif12  7505  tz7.44-1  8403  rdg0n  8431  resixpfo  8927  boxriin  8931  boxcutc  8932  pw2f1olem  9073  unxpdomlem2  9248  unxpdomlem3  9249  infsupprpr  9496  ordtypelem1  9510  wemaplem2  9539  unwdomg  9576  ixpiunwdom  9582  cantnfp1lem2  9671  cantnfp1lem3  9672  ssttrcl  9707  ttrclselem2  9718  acndom  10043  dfac12lem2  10136  fin23lem14  10325  axcc2lem  10428  pwfseqlem2  10651  uzin  12859  xrmax1  13151  xrmax2  13152  xrmin1  13153  xrmin2  13154  max1ALT  13162  max0sub  13172  ifle  13173  xmulneg1  13245  fzprval  13559  fztpval  13560  modifeq2int  13895  seqf1olem1  14004  seqf1olem2  14005  bcval2  14262  ccatval1  14524  ccatalpha  14540  swrdccat  14682  pfxccat3a  14685  swrdccat3b  14687  repswswrd  14731  cshword  14738  0csh0  14740  ccatco  14783  sgnn  15038  max0add  15254  absmax  15273  sumrblem  15654  fsumcvg  15655  summolem2a  15658  isum  15662  sumss  15667  sumss2  15669  fsumcvg2  15670  fsumser  15673  fsumsplit  15684  sumsplit  15711  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  zprod  15878  iprod  15879  iprodn0  15881  prodss  15888  fprodsplit  15907  ruclem2  16172  ruclem3  16173  flodddiv4  16353  sadadd2lem2  16388  sadcf  16391  sadc0  16392  sadcp1  16393  sadcaddlem  16395  smupf  16416  smup0  16417  gcd0val  16435  dfgcd2  16485  eucalgf  16517  eucalginv  16518  eucalglt  16519  lcmf0val  16556  phisum  16720  pc0  16784  pcgcd  16808  pcmptcl  16821  pcmpt  16822  pcmpt2  16823  pcprod  16825  fldivp1  16827  prmreclem2  16847  prmreclem4  16849  1arithlem4  16856  vdwlem6  16916  ramtcl2  16941  ramcl2  16946  ramub1lem1  16956  prmop1  16968  fvprmselelfz  16974  fvprmselgcd1  16975  ressid2  17174  xpsfrnel  17505  xpsaddlem  17516  xpsvsca  17520  mreexexd  17589  gsumval1  18599  mgm2nsgrplem2  18797  sgrp2nmndlem2  18802  symgextfve  19282  symgfixfolem1  19301  pmtrmvd  19319  pmtrfinv  19324  pmtrprfval  19350  pmtrprfvalrn  19351  frgpuptinv  19634  frgpup2  19639  frgpup3lem  19640  cyggex  19761  gsumzsplit  19790  gsummpt1n0  19828  dprdfid  19882  dmdprdsplitlem  19902  sdrgacs  20410  abvtrivd  20441  znf1o  21099  uvcvv1  21336  psrlidm  21515  psrridm  21516  mvrf1  21537  mplmonmul  21583  mplcoe1  21584  mplcoe3  21585  mplcoe5  21587  mplmon2  21614  subrgasclcl  21620  evlslem3  21635  evlslem1  21637  coe1tmfv1  21788  ply1sclid  21802  dmatmul  21991  scmatscmiddistr  22002  1mavmul  22042  mulmarep1gsum2  22068  1marepvmarrepid  22069  mdetdiag  22093  mdetralt2  22103  mdetunilem2  22107  mdetunilem7  22112  mdetunilem8  22113  mdetunilem9  22114  mndifsplit  22130  maducoeval2  22134  madugsum  22137  madurid  22138  gsummatr01lem3  22151  gsummatr01  22153  smadiadetglem2  22166  1elcpmat  22209  decpmatid  22264  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  ptpjpre1  23067  ptbasfi  23077  ptpjopn  23108  isfcls  23505  ptcmplem2  23549  ptcmplem3  23550  tsmssplit  23648  dscmet  24073  dscopn  24074  icccmplem2  24331  iccpnfcnv  24452  xrhmeo  24454  pcopt  24530  pcopt2  24531  pcoass  24532  pcorevlem  24534  cmetcaulem  24797  ovolicc1  25025  ioorcl  25086  i1f1lem  25198  itg11  25200  itg1addlem2  25206  itg1addlem4  25208  itg1addlem4OLD  25209  i1fres  25215  itg1climres  25224  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1flim  25233  itg2const2  25251  itg2seq  25252  itg2uba  25253  itg2splitlem  25258  itg2split  25259  itg2monolem1  25260  itg2cnlem1  25271  itg2cnlem2  25272  iblcnlem  25298  iblss  25314  iblss2  25315  itgitg2  25316  itgle  25319  itgss  25321  itgss2  25322  itgss3  25324  itgless  25326  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  iblabs  25338  iblabsr  25339  iblmulc2  25340  bddmulibl  25348  bddiblnc  25351  itggt0  25353  itgcn  25354  limcvallem  25380  ellimc2  25386  limccnp  25400  limccnp2  25401  limcco  25402  dvcobr  25455  dvexp2  25463  elply2  25702  elplyd  25708  ply1termlem  25709  coe1termlem  25764  abelthlem9  25944  logtayl  26160  leibpilem2  26436  leibpi  26437  rlimcnp2  26461  efrlim  26464  igamz  26542  isnsqf  26629  mule1  26642  sqff1o  26676  muinv  26687  chtublem  26704  dchrelbasd  26732  bposlem1  26777  bposlem3  26779  bposlem5  26781  bposlem6  26782  lgsval2lem  26800  lgsneg  26814  lgsdilem  26817  lgsdir2  26823  lgsdir  26825  lgsdi  26827  lgsne0  26828  gausslemma2dlem1a  26858  2lgslem1c  26886  2lgslem3  26897  2lgs  26900  dchrvmasum2if  26990  dchrvmasumiflem1  26994  rpvmasum2  27005  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  padicabv  27123  ostth2lem4  27129  nosupno  27196  nosupbday  27198  nosupbnd1  27207  nosupbnd2  27209  noinfno  27211  noinfbday  27213  noinfbnd1  27222  maxs1  27258  maxs2  27259  mins1  27260  mins2  27261  axlowdimlem15  28204  opvtxval  28253  opiedgval  28256  elimifd  31763  elim2if  31764  ifeq3da  31766  ifnefals  31768  pmtridf1o  32241  fzto1stfv1  32248  resvid2  32431  xrge0iifcnv  32902  xrge0iifiso  32904  xrge0iifhom  32906  indval2  33001  ind1  33004  sigaclfu2  33108  ddeval1  33221  eulerpartlemb  33356  ballotlemsima  33503  ballotlemrv1  33508  signsw0glem  33553  signswmnd  33557  signswrid  33558  indispconn  34214  ex-sategoelel  34401  ex-sategoelelomsuc  34406  ex-sategoelel12  34407  mrsubvr  34491  dfrdg2  34756  dfrdg3  34757  unisnif  34886  dfrdg4  34912  gg-dvcobr  35165  fnejoin2  35243  unbdqndv2lem2  35375  bj-xpima2sn  35828  finxpreclem1  36259  finxpreclem3  36263  matunitlindflem1  36473  poimirlem2  36479  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem24  36501  mblfinlem2  36515  mbfposadd  36524  itg2addnclem  36528  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itggt0cn  36547  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  areacirclem5  36569  areacirc  36570  fdc  36602  heiborlem4  36671  ac6s6  37029  cdleme27a  39227  cdleme31sn1  39241  cdleme31fv1  39251  cdlemk40t  39778  dihvalb  40097  sticksstones12a  40962  metakunt5  40978  metakunt6  40979  metakunt10  40983  metakunt11  40984  metakunt20  40993  brif1  41038  brif2  41039  brif12  41040  evlsbagval  41136  selvvvval  41155  fsuppind  41160  dffltz  41373  pw2f1ocnv  41762  aomclem5  41786  kelac1  41791  mon1pid  41933  arearect  41950  areaquad  41951  oe0rif  42021  cantnfresb  42060  safesnsupfidom1o  42154  safesnsupfilb  42155  clsk1indlem1  42782  refsum2cnlem1  43707  upbdrech2  44005  lptioo2  44334  lptioo1  44335  limsupmnfuzlem  44429  limsupre3uzlem  44438  limsup10exlem  44475  coskpi2  44569  cosknegpi  44572  cncfiooicclem1  44596  cncfiooiccre  44598  dvnxpaek  44645  dvnprodlem1  44649  dvnprodlem3  44651  itgioocnicc  44680  iblcncfioo  44681  volico  44686  sublevolico  44687  volioore  44693  voliooico  44695  voliccico  44702  dirkerper  44799  dirkertrigeq  44804  dirkercncflem2  44807  fourierdlem10  44820  fourierdlem32  44842  fourierdlem33  44843  fourierdlem37  44847  fourierdlem62  44871  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem93  44902  fourierdlem97  44906  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  fouriersw  44934  etransclem4  44941  etransclem15  44952  etransclem19  44956  etransclem20  44957  etransclem23  44960  etransclem24  44961  etransclem25  44962  etransclem27  44964  etransclem31  44968  etransclem32  44969  ioorrnopnxrlem  45009  nnfoctbdjlem  45158  isomenndlem  45233  ovn0val  45253  hoidmv0val  45286  hsphoidmvle2  45288  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1le  45297  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoilem1  45304  hspdifhsp  45319  hoidifhspdmvle  45323  hspmbllem1  45329  hspmbllem2  45330  hspmbl  45332  volico2  45344  ovnsubadd2lem  45348  ovolval4lem2  45353  ovolval5lem1  45355  afvfundmfveq  45833  dfatafv2iota  45905  dfatafv2eqfv  45956  prproropf1olem3  46160  prproropf1olem4  46161  linc1  47060  lincext3  47091  lindslinindsimp1  47092  el0ldep  47101  islindeps2  47118  itcoval0  47302  ackval0  47320