Theorem iftrue 4042

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		dedlem0a 991	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
2	1	abbi2dv 2729	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
3		dfif2 4038	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
4	2, 3	syl6reqr 2663	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  iftruei  4043  iftrued  4044  ifsb  4049  ifbi  4057  ifeq2da  4067  ifeq12da  4068  ifclda  4070  ifeqda  4071  elimif  4072  ifbothda  4073  ifid  4075  ifeqor  4082  ifnot  4083  ifan  4084  ifor  4085  2if2  4086  dedth  4089  elimhyp  4096  elimhyp2v  4097  elimhyp3v  4098  elimhyp4v  4099  elimdhyp  4101  keephyp2v  4103  keephyp3v  4104  dfopif  4337  dfopg  4338  somin1  5448  somincom  5449  xpima1  5496  dfiota4  5796  elimdelov  6634  ovif12  6637  tz7.44-1  7389  resixpfo  7832  boxriin  7836  boxcutc  7837  pw2f1olem  7949  unxpdomlem2  8050  unxpdomlem3  8051  ordtypelem1  8306  wemaplem2  8335  unwdomg  8372  ixpiunwdom  8379  cantnfp1lem2  8459  cantnfp1lem3  8460  acndom  8757  dfac12lem2  8849  fin23lem14  9038  axcc2lem  9141  pwfseqlem2  9360  uzin  11596  xrmax1  11880  xrmax2  11881  xrmin1  11882  xrmin2  11883  max1ALT  11891  max0sub  11901  ifle  11902  xmulneg1  11971  fzprval  12271  fztpval  12272  modifeq2int  12594  seqf1olem1  12702  seqf1olem2  12703  bcval2  12954  ccatval1  13214  ccatalpha  13228  swrdccat  13344  swrdccat3a  13345  swrdccat3b  13347  repswswrd  13382  cshword  13388  0csh0  13390  ccatco  13432  sgnn  13682  max0add  13898  absmax  13917  sumrblem  14289  fsumcvg  14290  summolem2a  14293  isum  14297  sumss  14302  sumss2  14304  fsumcvg2  14305  fsumser  14308  fsumsplit  14318  sumsplit  14341  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  zprod  14506  iprod  14507  iprodn0  14509  prodss  14516  fprodsplit  14535  ruclem2  14800  ruclem3  14801  flodddiv4  14975  sadadd2lem2  15010  sadcf  15013  sadc0  15014  sadcp1  15015  sadcaddlem  15017  smupf  15038  smup0  15039  gcd0val  15057  dfgcd2  15101  eucalgf  15134  eucalginv  15135  eucalglt  15136  lcmf0val  15173  phisum  15333  pc0  15397  pcgcd  15420  pcmptcl  15433  pcmpt  15434  pcmpt2  15435  pcprod  15437  fldivp1  15439  prmreclem2  15459  prmreclem4  15461  1arithlem4  15468  vdwlem6  15528  ramtcl2  15553  ramcl2  15558  ramub1lem1  15568  prmop1  15580  fvprmselelfz  15586  fvprmselgcd1  15587  ressid2  15755  xpscfv  16045  xpsfrnel  16046  xpsaddlem  16058  xpsvsca  16062  mreexexd  16131  gsumval1  17100  mgm2nsgrplem2  17229  sgrp2nmndlem2  17234  symgextfve  17662  symgfixfolem1  17681  pmtrmvd  17699  pmtrfinv  17704  pmtrprfval  17730  pmtrprfvalrn  17731  frgpuptinv  18007  frgpup2  18012  frgpup3lem  18013  cyggex  18122  gsumzsplit  18150  gsummpt1n0  18187  dprdfid  18239  dmdprdsplitlem  18259  abvtrivd  18663  psrlidm  19224  psrridm  19225  mvrf1  19246  mplmonmul  19285  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  mplmon2  19314  subrgasclcl  19320  evlslem3  19335  evlslem1  19336  coe1tmfv1  19465  ply1sclid  19479  znf1o  19719  uvcvv1  19947  dmatmul  20122  scmatscmiddistr  20133  1mavmul  20173  mulmarep1gsum2  20199  1marepvmarrepid  20200  mdetdiag  20224  mdetralt2  20234  mdetunilem2  20238  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  mndifsplit  20261  maducoeval2  20265  madugsum  20268  madurid  20269  gsummatr01lem3  20282  gsummatr01  20284  smadiadetglem2  20297  1elcpmat  20339  decpmatid  20394  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  ptpjpre1  21184  ptbasfi  21194  ptpjopn  21225  isfcls  21623  ptcmplem2  21667  ptcmplem3  21668  tsmssplit  21765  dscmet  22187  dscopn  22188  icccmplem2  22434  iccpnfcnv  22551  xrhmeo  22553  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  cmetcaulem  22894  ovolicc1  23091  ioorcl  23151  i1f1lem  23262  itg11  23264  itg1addlem2  23270  itg1addlem4  23272  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1flim  23296  itg2const2  23314  itg2seq  23315  itg2uba  23316  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2cnlem1  23334  itg2cnlem2  23335  iblcnlem  23361  iblss  23377  iblss2  23378  itgitg2  23379  itgle  23382  itgss  23384  itgss2  23385  itgss3  23387  itgless  23389  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  bddmulibl  23411  itggt0  23414  itgcn  23415  limcvallem  23441  ellimc2  23447  limccnp  23461  limccnp2  23462  limcco  23463  dvcobr  23515  dvexp2  23523  elply2  23756  elplyd  23762  ply1termlem  23763  coe1termlem  23818  abelthlem9  23998  logtayl  24206  leibpilem2  24468  leibpi  24469  rlimcnp2  24493  efrlim  24496  igamz  24574  isnsqf  24661  mule1  24674  sqff1o  24708  muinv  24719  chtublem  24736  dchrelbasd  24764  bposlem1  24809  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgsval2lem  24832  lgsneg  24846  lgsdilem  24849  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsne0  24860  gausslemma2dlem1a  24890  2lgslem1c  24918  2lgslem3  24929  2lgs  24932  dchrvmasum2if  24986  dchrvmasumiflem1  24990  rpvmasum2  25001  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  padicabv  25119  ostth2lem4  25125  axlowdimlem15  25636  opvtxval  25680  opiedgval  25683  elimifd  28746  elim2if  28747  resvid2  29159  fzto1stfv1  29182  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  indval2  29404  ind1  29408  sigaclfu2  29511  ddeval1  29624  eulerpartlemb  29757  ballotlemsima  29904  ballotlemrv1  29909  signsw0glem  29956  signswmnd  29960  signswrid  29961  indispcon  30470  mrsubvr  30662  dfrdg2  30945  dfrdg3  30946  unisnif  31202  dfrdg4  31228  fnejoin2  31534  unbdqndv2lem2  31671  bj-xpima2sn  32138  finxpreclem1  32402  finxpreclem3  32406  matunitlindflem1  32575  poimirlem2  32581  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  mblfinlem2  32617  mbfposadd  32627  itg2addnclem  32631  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem1  32638  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  bddiblnc  32650  itggt0cn  32652  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem5  32674  areacirc  32675  fdc  32711  heiborlem4  32783  ac6s6  33150  cdleme27a  34673  cdleme31sn1  34687  cdleme31fv1  34697  cdlemk40t  35224  dihvalb  35544  pw2f1ocnv  36622  aomclem5  36646  kelac1  36651  sdrgacs  36790  mon1pid  36802  arearect  36820  areaquad  36821  clsk1indlem1  37363  refsum2cnlem1  38219  upbdrech2  38463  lptioo2  38698  lptioo1  38699  coskpi2  38749  cosknegpi  38752  cncfiooicclem1  38779  cncfiooiccre  38781  dvnxpaek  38832  dvnprodlem1  38836  dvnprodlem3  38838  itgioocnicc  38869  iblcncfioo  38870  volico  38876  sublevolico  38877  volioore  38883  voliooico  38885  voliccico  38892  dirkerper  38989  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem10  39010  fourierdlem32  39032  fourierdlem33  39033  fourierdlem37  39037  fourierdlem62  39061  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem93  39092  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem4  39131  etransclem15  39142  etransclem19  39146  etransclem20  39147  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem27  39154  etransclem31  39158  etransclem32  39159  ioorrnopnxrlem  39202  nnfoctbdjlem  39348  isomenndlem  39420  ovn0val  39440  hoidmv0val  39473  hsphoidmvle2  39475  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  hspdifhsp  39506  hoidifhspdmvle  39510  hspmbllem1  39516  hspmbllem2  39517  hspmbl  39519  volico2  39531  ovnsubadd2lem  39535  ovolval4lem2  39540  ovolval5lem1  39542  afvfundmfveq  39867  pfxccat3a  40292  cshword2  40300  linc1  42008  lincext3  42039  lindslinindsimp1  42040  el0ldep  42049  islindeps2  42066