Theorem iftrue 4497

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2708  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-if 4492

This theorem is referenced by:  iftruei  4498  iftrued  4499  ifsb  4504  ifbi  4513  ifeq2da  4523  ifeq12da  4524  ifclda  4526  ifeqda  4527  elimif  4528  ifbothda  4529  ifid  4531  ifeqor  4542  ifnot  4543  ifan  4544  ifor  4545  2if2  4546  dedth  4549  elimhyp  4556  elimhyp2v  4557  elimhyp3v  4558  elimhyp4v  4559  elimdhyp  4561  keephyp2v  4563  keephyp3v  4564  dfopif  4832  dfopg  4833  somin1  6092  somincom  6093  xpima1  6140  elimdelov  7458  ovif12  7461  tz7.44-1  8357  rdg0n  8385  resixpfo  8881  boxriin  8885  boxcutc  8886  pw2f1olem  9027  unxpdomlem2  9202  unxpdomlem3  9203  infsupprpr  9449  ordtypelem1  9463  wemaplem2  9492  unwdomg  9529  ixpiunwdom  9535  cantnfp1lem2  9624  cantnfp1lem3  9625  ssttrcl  9660  ttrclselem2  9671  acndom  9996  dfac12lem2  10089  fin23lem14  10278  axcc2lem  10381  pwfseqlem2  10604  uzin  12812  xrmax1  13104  xrmax2  13105  xrmin1  13106  xrmin2  13107  max1ALT  13115  max0sub  13125  ifle  13126  xmulneg1  13198  fzprval  13512  fztpval  13513  modifeq2int  13848  seqf1olem1  13957  seqf1olem2  13958  bcval2  14215  ccatval1  14477  ccatalpha  14493  swrdccat  14635  pfxccat3a  14638  swrdccat3b  14640  repswswrd  14684  cshword  14691  0csh0  14693  ccatco  14736  sgnn  14991  max0add  15207  absmax  15226  sumrblem  15607  fsumcvg  15608  summolem2a  15611  isum  15615  sumss  15620  sumss2  15622  fsumcvg2  15623  fsumser  15626  fsumsplit  15637  sumsplit  15664  prodrblem  15823  fprodcvg  15824  prodmolem2a  15828  zprod  15831  iprod  15832  iprodn0  15834  prodss  15841  fprodsplit  15860  ruclem2  16125  ruclem3  16126  flodddiv4  16306  sadadd2lem2  16341  sadcf  16344  sadc0  16345  sadcp1  16346  sadcaddlem  16348  smupf  16369  smup0  16370  gcd0val  16388  dfgcd2  16438  eucalgf  16470  eucalginv  16471  eucalglt  16472  lcmf0val  16509  phisum  16673  pc0  16737  pcgcd  16761  pcmptcl  16774  pcmpt  16775  pcmpt2  16776  pcprod  16778  fldivp1  16780  prmreclem2  16800  prmreclem4  16802  1arithlem4  16809  vdwlem6  16869  ramtcl2  16894  ramcl2  16899  ramub1lem1  16909  prmop1  16921  fvprmselelfz  16927  fvprmselgcd1  16928  ressid2  17127  xpsfrnel  17458  xpsaddlem  17469  xpsvsca  17473  mreexexd  17542  gsumval1  18552  mgm2nsgrplem2  18743  sgrp2nmndlem2  18748  symgextfve  19215  symgfixfolem1  19234  pmtrmvd  19252  pmtrfinv  19257  pmtrprfval  19283  pmtrprfvalrn  19284  frgpuptinv  19567  frgpup2  19572  frgpup3lem  19573  cyggex  19689  gsumzsplit  19718  gsummpt1n0  19756  dprdfid  19810  dmdprdsplitlem  19830  sdrgacs  20324  abvtrivd  20355  znf1o  20995  uvcvv1  21232  psrlidm  21409  psrridm  21410  mvrf1  21431  mplmonmul  21474  mplcoe1  21475  mplcoe3  21476  mplcoe5  21478  mplmon2  21506  subrgasclcl  21512  evlslem3  21527  evlslem1  21529  coe1tmfv1  21682  ply1sclid  21696  dmatmul  21883  scmatscmiddistr  21894  1mavmul  21934  mulmarep1gsum2  21960  1marepvmarrepid  21961  mdetdiag  21985  mdetralt2  21995  mdetunilem2  21999  mdetunilem7  22004  mdetunilem8  22005  mdetunilem9  22006  mndifsplit  22022  maducoeval2  22026  madugsum  22029  madurid  22030  gsummatr01lem3  22043  gsummatr01  22045  smadiadetglem2  22058  1elcpmat  22101  decpmatid  22156  chfacfscmulgsum  22246  chfacfpmmulgsum  22250  ptpjpre1  22959  ptbasfi  22969  ptpjopn  23000  isfcls  23397  ptcmplem2  23441  ptcmplem3  23442  tsmssplit  23540  dscmet  23965  dscopn  23966  icccmplem2  24223  iccpnfcnv  24344  xrhmeo  24346  pcopt  24422  pcopt2  24423  pcoass  24424  pcorevlem  24426  cmetcaulem  24689  ovolicc1  24917  ioorcl  24978  i1f1lem  25090  itg11  25092  itg1addlem2  25098  itg1addlem4  25100  itg1addlem4OLD  25101  i1fres  25107  itg1climres  25116  mbfi1fseqlem4  25120  mbfi1fseqlem5  25121  mbfi1flim  25125  itg2const2  25143  itg2seq  25144  itg2uba  25145  itg2splitlem  25150  itg2split  25151  itg2monolem1  25152  itg2cnlem1  25163  itg2cnlem2  25164  iblcnlem  25190  iblss  25206  iblss2  25207  itgitg2  25208  itgle  25211  itgss  25213  itgss2  25214  itgss3  25216  itgless  25218  ibladdlem  25221  itgaddlem1  25224  iblabslem  25229  iblabs  25230  iblabsr  25231  iblmulc2  25232  bddmulibl  25240  bddiblnc  25243  itggt0  25245  itgcn  25246  limcvallem  25272  ellimc2  25278  limccnp  25292  limccnp2  25293  limcco  25294  dvcobr  25347  dvexp2  25355  elply2  25594  elplyd  25600  ply1termlem  25601  coe1termlem  25656  abelthlem9  25836  logtayl  26052  leibpilem2  26328  leibpi  26329  rlimcnp2  26353  efrlim  26356  igamz  26434  isnsqf  26521  mule1  26534  sqff1o  26568  muinv  26579  chtublem  26596  dchrelbasd  26624  bposlem1  26669  bposlem3  26671  bposlem5  26673  bposlem6  26674  lgsval2lem  26692  lgsneg  26706  lgsdilem  26709  lgsdir2  26715  lgsdir  26717  lgsdi  26719  lgsne0  26720  gausslemma2dlem1a  26750  2lgslem1c  26778  2lgslem3  26789  2lgs  26792  dchrvmasum2if  26882  dchrvmasumiflem1  26886  rpvmasum2  26897  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  padicabv  27015  ostth2lem4  27021  nosupno  27088  nosupbday  27090  nosupbnd1  27099  nosupbnd2  27101  noinfno  27103  noinfbday  27105  noinfbnd1  27114  maxs1  27150  maxs2  27151  mins1  27152  mins2  27153  axlowdimlem15  27968  opvtxval  28017  opiedgval  28020  elimifd  31529  elim2if  31530  ifeq3da  31532  ifnefals  31534  pmtridf1o  32013  fzto1stfv1  32020  resvid2  32190  xrge0iifcnv  32603  xrge0iifiso  32605  xrge0iifhom  32607  indval2  32702  ind1  32705  sigaclfu2  32809  ddeval1  32922  eulerpartlemb  33057  ballotlemsima  33204  ballotlemrv1  33209  signsw0glem  33254  signswmnd  33258  signswrid  33259  indispconn  33915  ex-sategoelel  34102  ex-sategoelelomsuc  34107  ex-sategoelel12  34108  mrsubvr  34192  dfrdg2  34456  dfrdg3  34457  unisnif  34586  dfrdg4  34612  fnejoin2  34917  unbdqndv2lem2  35049  bj-xpima2sn  35502  finxpreclem1  35933  finxpreclem3  35937  matunitlindflem1  36147  poimirlem2  36153  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem24  36175  mblfinlem2  36189  mbfposadd  36198  itg2addnclem  36202  itg2gt0cn  36206  ibladdnclem  36207  itgaddnclem1  36209  iblabsnclem  36214  iblabsnc  36215  iblmulc2nc  36216  itggt0cn  36221  ftc1anclem4  36227  ftc1anclem5  36228  ftc1anclem6  36229  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  areacirclem5  36243  areacirc  36244  fdc  36277  heiborlem4  36346  ac6s6  36704  cdleme27a  38903  cdleme31sn1  38917  cdleme31fv1  38927  cdlemk40t  39454  dihvalb  39773  sticksstones12a  40638  metakunt5  40654  metakunt6  40655  metakunt10  40659  metakunt11  40660  metakunt20  40669  brif1  40717  brif2  40718  brif12  40719  evlsbagval  40806  fsuppind  40823  dffltz  41030  pw2f1ocnv  41419  aomclem5  41443  kelac1  41448  mon1pid  41590  arearect  41607  areaquad  41608  oe0rif  41678  cantnfresb  41717  safesnsupfidom1o  41811  safesnsupfilb  41812  clsk1indlem1  42439  refsum2cnlem1  43364  upbdrech2  43663  lptioo2  43992  lptioo1  43993  limsupmnfuzlem  44087  limsupre3uzlem  44096  limsup10exlem  44133  coskpi2  44227  cosknegpi  44230  cncfiooicclem1  44254  cncfiooiccre  44256  dvnxpaek  44303  dvnprodlem1  44307  dvnprodlem3  44309  itgioocnicc  44338  iblcncfioo  44339  volico  44344  sublevolico  44345  volioore  44351  voliooico  44353  voliccico  44360  dirkerper  44457  dirkertrigeq  44462  dirkercncflem2  44465  fourierdlem10  44478  fourierdlem32  44500  fourierdlem33  44501  fourierdlem37  44505  fourierdlem62  44529  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem79  44546  fourierdlem81  44548  fourierdlem82  44549  fourierdlem93  44560  fourierdlem97  44564  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  sqwvfoura  44589  sqwvfourb  44590  fourierswlem  44591  fouriersw  44592  etransclem4  44599  etransclem15  44610  etransclem19  44614  etransclem20  44615  etransclem23  44618  etransclem24  44619  etransclem25  44620  etransclem27  44622  etransclem31  44626  etransclem32  44627  ioorrnopnxrlem  44667  nnfoctbdjlem  44816  isomenndlem  44891  ovn0val  44911  hoidmv0val  44944  hsphoidmvle2  44946  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1le  44955  hoidmvlelem2  44957  hoidmvlelem3  44958  ovnhoilem1  44962  hspdifhsp  44977  hoidifhspdmvle  44981  hspmbllem1  44987  hspmbllem2  44988  hspmbl  44990  volico2  45002  ovnsubadd2lem  45006  ovolval4lem2  45011  ovolval5lem1  45013  afvfundmfveq  45490  dfatafv2iota  45562  dfatafv2eqfv  45613  prproropf1olem3  45817  prproropf1olem4  45818  linc1  46626  lincext3  46657  lindslinindsimp1  46658  el0ldep  46667  islindeps2  46684  itcoval0  46868  ackval0  46886