Theorem iftrue 4536

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {cab 2711  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  iftruei  4537  iftrued  4538  ifsb  4543  ifbi  4552  ifeq2da  4562  ifeq12da  4563  ifclda  4565  ifeqda  4566  elimif  4567  ifbothda  4568  ifid  4570  ifeqor  4581  ifnot  4582  ifan  4583  ifor  4584  2if2  4585  dedth  4588  elimhyp  4595  elimhyp2v  4596  elimhyp3v  4597  elimhyp4v  4598  elimdhyp  4600  keephyp2v  4602  keephyp3v  4603  dfopif  4874  dfopg  4875  somin1  6155  somincom  6156  xpima1  6204  elimdelov  7528  brif1  7529  ovif12  7532  tz7.44-1  8444  rdg0n  8472  resixpfo  8974  boxriin  8978  boxcutc  8979  pw2f1olem  9114  unxpdomlem2  9284  unxpdomlem3  9285  infsupprpr  9541  ordtypelem1  9555  wemaplem2  9584  unwdomg  9621  ixpiunwdom  9627  cantnfp1lem2  9716  cantnfp1lem3  9717  ssttrcl  9752  ttrclselem2  9763  acndom  10088  dfac12lem2  10182  fin23lem14  10370  axcc2lem  10473  pwfseqlem2  10696  uzin  12915  xrmax1  13213  xrmax2  13214  xrmin1  13215  xrmin2  13216  max1ALT  13224  max0sub  13234  ifle  13235  xmulneg1  13307  fzprval  13621  fztpval  13622  modifeq2int  13970  seqf1olem1  14078  seqf1olem2  14079  bcval2  14340  tpf1ofv0  14531  tpf1ofv1  14532  ccatval1  14611  ccatalpha  14627  swrdccat  14769  pfxccat3a  14772  swrdccat3b  14774  repswswrd  14818  cshword  14825  0csh0  14827  ccatco  14870  sgnn  15129  max0add  15345  absmax  15364  sumrblem  15743  fsumcvg  15744  summolem2a  15747  isum  15751  sumss  15756  sumss2  15758  fsumcvg2  15759  fsumser  15762  fsumsplit  15773  sumsplit  15800  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  iprod  15970  iprodn0  15972  prodss  15979  fprodsplit  15998  ruclem2  16264  ruclem3  16265  flodddiv4  16448  sadadd2lem2  16483  sadcf  16486  sadc0  16487  sadcp1  16488  sadcaddlem  16490  smupf  16511  smup0  16512  gcd0val  16530  dfgcd2  16579  eucalgf  16616  eucalginv  16617  eucalglt  16618  lcmf0val  16655  phisum  16823  pc0  16887  pcgcd  16911  pcmptcl  16924  pcmpt  16925  pcmpt2  16926  pcprod  16928  fldivp1  16930  prmreclem2  16950  prmreclem4  16952  1arithlem4  16959  vdwlem6  17019  ramtcl2  17044  ramcl2  17049  ramub1lem1  17059  prmop1  17071  fvprmselelfz  17077  fvprmselgcd1  17078  ressid2  17277  xpsfrnel  17608  xpsaddlem  17619  xpsvsca  17623  mreexexd  17692  gsumval1  18708  mgm2nsgrplem2  18944  sgrp2nmndlem2  18949  symgextfve  19451  symgfixfolem1  19470  pmtrmvd  19488  pmtrfinv  19493  pmtrprfval  19519  pmtrprfvalrn  19520  frgpuptinv  19803  frgpup2  19808  frgpup3lem  19809  cyggex  19930  gsumzsplit  19959  gsummpt1n0  19997  dprdfid  20051  dmdprdsplitlem  20071  sdrgacs  20818  abvtrivd  20849  znf1o  21587  uvcvv1  21826  psrlidm  21999  psrridm  22000  mvrf1  22023  mplmonmul  22071  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  mplmon2  22102  subrgasclcl  22108  evlslem3  22121  evlslem1  22123  psdmul  22187  coe1tmfv1  22292  ply1sclid  22306  dmatmul  22518  scmatscmiddistr  22529  1mavmul  22569  mulmarep1gsum2  22595  1marepvmarrepid  22596  mdetdiag  22620  mdetralt2  22630  mdetunilem2  22634  mdetunilem7  22639  mdetunilem8  22640  mdetunilem9  22641  mndifsplit  22657  maducoeval2  22661  madugsum  22664  madurid  22665  gsummatr01lem3  22678  gsummatr01  22680  smadiadetglem2  22693  1elcpmat  22736  decpmatid  22791  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  ptpjpre1  23594  ptbasfi  23604  ptpjopn  23635  isfcls  24032  ptcmplem2  24076  ptcmplem3  24077  tsmssplit  24175  dscmet  24600  dscopn  24601  icccmplem2  24858  iccpnfcnv  24988  xrhmeo  24990  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  cmetcaulem  25335  ovolicc1  25564  ioorcl  25625  i1f1lem  25737  itg11  25739  itg1addlem2  25745  itg1addlem4  25747  itg1addlem4OLD  25748  i1fres  25754  itg1climres  25763  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1flim  25772  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2cnlem1  25810  itg2cnlem2  25811  iblcnlem  25838  iblss  25854  iblss2  25855  itgitg2  25856  itgle  25859  itgss  25861  itgss2  25862  itgss3  25864  itgless  25866  ibladdlem  25869  itgaddlem1  25872  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  bddmulibl  25888  bddiblnc  25891  itggt0  25893  itgcn  25894  limcvallem  25920  ellimc2  25926  limccnp  25940  limccnp2  25941  limcco  25942  dvcobr  25997  dvcobrOLD  25998  dvexp2  26006  mon1pid  26207  elply2  26249  elplyd  26255  ply1termlem  26256  coe1termlem  26311  abelthlem9  26498  logtayl  26716  leibpilem2  26998  leibpi  26999  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  igamz  27105  isnsqf  27192  mule1  27205  sqff1o  27239  muinv  27250  chtublem  27269  dchrelbasd  27297  bposlem1  27342  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgsval2lem  27365  lgsneg  27379  lgsdilem  27382  lgsdir2  27388  lgsdir  27390  lgsdi  27392  lgsne0  27393  gausslemma2dlem1a  27423  2lgslem1c  27451  2lgslem3  27462  2lgs  27465  dchrvmasum2if  27555  dchrvmasumiflem1  27559  rpvmasum2  27570  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  padicabv  27688  ostth2lem4  27694  nosupno  27762  nosupbday  27764  nosupbnd1  27773  nosupbnd2  27775  noinfno  27777  noinfbday  27779  noinfbnd1  27788  maxs1  27824  maxs2  27825  mins1  27826  mins2  27827  abssid  28279  abssge0  28283  axlowdimlem15  28985  opvtxval  29034  opiedgval  29037  elimifd  32563  elim2if  32564  ifeq3da  32566  ifnefals  32568  fmptunsnop  32714  pmtridf1o  33096  fzto1stfv1  33103  resvid2  33333  2sqr3minply  33752  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  indval2  33994  ind1  33997  sigaclfu2  34101  ddeval1  34214  eulerpartlemb  34349  ballotlemsima  34496  ballotlemrv1  34501  signsw0glem  34546  signswmnd  34550  signswrid  34551  indispconn  35218  ex-sategoelel  35405  ex-sategoelelomsuc  35410  ex-sategoelel12  35411  mrsubvr  35495  dfrdg2  35776  dfrdg3  35777  unisnif  35906  dfrdg4  35932  fnejoin2  36351  unbdqndv2lem2  36492  bj-xpima2sn  36940  finxpreclem1  37371  finxpreclem3  37375  matunitlindflem1  37602  poimirlem2  37608  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  mblfinlem2  37644  mbfposadd  37653  itg2addnclem  37657  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem1  37664  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  itggt0cn  37676  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirclem5  37698  areacirc  37699  fdc  37731  heiborlem4  37800  ac6s6  38158  cdleme27a  40349  cdleme31sn1  40363  cdleme31fv1  40373  cdlemk40t  40900  dihvalb  41219  sticksstones12a  42138  metakunt5  42190  metakunt6  42191  metakunt10  42195  metakunt11  42196  metakunt20  42205  brif2  42241  brif12  42242  evlsbagval  42552  selvvvval  42571  fsuppind  42576  dffltz  42620  pw2f1ocnv  43025  aomclem5  43046  kelac1  43051  arearect  43203  areaquad  43204  oe0rif  43274  cantnfresb  43313  safesnsupfidom1o  43406  safesnsupfilb  43407  clsk1indlem1  44034  refsum2cnlem1  44974  upbdrech2  45258  lptioo2  45586  lptioo1  45587  limsupmnfuzlem  45681  limsupre3uzlem  45690  limsup10exlem  45727  coskpi2  45821  cosknegpi  45824  cncfiooicclem1  45848  cncfiooiccre  45850  dvnxpaek  45897  dvnprodlem1  45901  dvnprodlem3  45903  itgioocnicc  45932  iblcncfioo  45933  volico  45938  sublevolico  45939  volioore  45945  voliooico  45947  voliccico  45954  dirkerper  46051  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem10  46072  fourierdlem32  46094  fourierdlem33  46095  fourierdlem37  46099  fourierdlem62  46123  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem93  46154  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem4  46193  etransclem15  46204  etransclem19  46208  etransclem20  46209  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem27  46216  etransclem31  46220  etransclem32  46221  ioorrnopnxrlem  46261  nnfoctbdjlem  46410  isomenndlem  46485  ovn0val  46505  hoidmv0val  46538  hsphoidmvle2  46540  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1le  46549  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  hspdifhsp  46571  hoidifhspdmvle  46575  hspmbllem1  46581  hspmbllem2  46582  hspmbl  46584  volico2  46596  ovnsubadd2lem  46600  ovolval4lem2  46605  ovolval5lem1  46607  afvfundmfveq  47087  dfatafv2iota  47159  dfatafv2eqfv  47210  prproropf1olem3  47429  prproropf1olem4  47430  linc1  48270  lincext3  48301  lindslinindsimp1  48302  el0ldep  48311  islindeps2  48328  itcoval0  48511  ackval0  48529