Theorem iftrue 4431

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 4427	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
2		dedlem0a 1039	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
3	2	abbi2dv 2927	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
4	1, 3	eqtr4id 2852	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  ifcif 4425

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  iftruei  4432  iftrued  4433  ifsb  4438  ifbi  4446  ifeq2da  4456  ifeq12da  4457  ifclda  4459  ifeqda  4460  elimif  4461  ifbothda  4462  ifid  4464  ifeqor  4474  ifnot  4475  ifan  4476  ifor  4477  2if2  4478  dedth  4481  elimhyp  4488  elimhyp2v  4489  elimhyp3v  4490  elimhyp4v  4491  elimdhyp  4493  keephyp2v  4495  keephyp3v  4496  dfopif  4760  dfopg  4761  somin1  5960  somincom  5961  xpima1  6007  elimdelov  7229  ovif12  7232  tz7.44-1  8025  resixpfo  8483  boxriin  8487  boxcutc  8488  pw2f1olem  8604  unxpdomlem2  8707  unxpdomlem3  8708  infsupprpr  8952  ordtypelem1  8966  wemaplem2  8995  unwdomg  9032  ixpiunwdom  9038  cantnfp1lem2  9126  cantnfp1lem3  9127  acndom  9462  dfac12lem2  9555  fin23lem14  9744  axcc2lem  9847  pwfseqlem2  10070  uzin  12266  xrmax1  12556  xrmax2  12557  xrmin1  12558  xrmin2  12559  max1ALT  12567  max0sub  12577  ifle  12578  xmulneg1  12650  fzprval  12963  fztpval  12964  modifeq2int  13296  seqf1olem1  13405  seqf1olem2  13406  bcval2  13661  ccatval1  13921  ccatval1OLD  13922  ccatalpha  13938  swrdccat  14088  pfxccat3a  14091  swrdccat3b  14093  repswswrd  14137  cshword  14144  0csh0  14146  ccatco  14188  sgnn  14445  max0add  14662  absmax  14681  sumrblem  15060  fsumcvg  15061  summolem2a  15064  isum  15068  sumss  15073  sumss2  15075  fsumcvg2  15076  fsumser  15079  fsumsplit  15089  sumsplit  15115  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  iprod  15284  iprodn0  15286  prodss  15293  fprodsplit  15312  ruclem2  15577  ruclem3  15578  flodddiv4  15754  sadadd2lem2  15789  sadcf  15792  sadc0  15793  sadcp1  15794  sadcaddlem  15796  smupf  15817  smup0  15818  gcd0val  15836  dfgcd2  15884  eucalgf  15917  eucalginv  15918  eucalglt  15919  lcmf0val  15956  phisum  16117  pc0  16181  pcgcd  16204  pcmptcl  16217  pcmpt  16218  pcmpt2  16219  pcprod  16221  fldivp1  16223  prmreclem2  16243  prmreclem4  16245  1arithlem4  16252  vdwlem6  16312  ramtcl2  16337  ramcl2  16342  ramub1lem1  16352  prmop1  16364  fvprmselelfz  16370  fvprmselgcd1  16371  ressid2  16544  xpsfrnel  16827  xpsaddlem  16838  xpsvsca  16842  mreexexd  16911  gsumval1  17885  mgm2nsgrplem2  18076  sgrp2nmndlem2  18081  symgextfve  18539  symgfixfolem1  18558  pmtrmvd  18576  pmtrfinv  18581  pmtrprfval  18607  pmtrprfvalrn  18608  frgpuptinv  18889  frgpup2  18894  frgpup3lem  18895  cyggex  19011  gsumzsplit  19040  gsummpt1n0  19078  dprdfid  19132  dmdprdsplitlem  19152  sdrgacs  19573  abvtrivd  19604  znf1o  20243  uvcvv1  20478  psrlidm  20641  psrridm  20642  mvrf1  20663  mplmonmul  20704  mplcoe1  20705  mplcoe3  20706  mplcoe5  20708  mplmon2  20732  subrgasclcl  20738  evlslem3  20752  evlslem1  20754  coe1tmfv1  20903  ply1sclid  20917  dmatmul  21102  scmatscmiddistr  21113  1mavmul  21153  mulmarep1gsum2  21179  1marepvmarrepid  21180  mdetdiag  21204  mdetralt2  21214  mdetunilem2  21218  mdetunilem7  21223  mdetunilem8  21224  mdetunilem9  21225  mndifsplit  21241  maducoeval2  21245  madugsum  21248  madurid  21249  gsummatr01lem3  21262  gsummatr01  21264  smadiadetglem2  21277  1elcpmat  21320  decpmatid  21375  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  ptpjpre1  22176  ptbasfi  22186  ptpjopn  22217  isfcls  22614  ptcmplem2  22658  ptcmplem3  22659  tsmssplit  22757  dscmet  23179  dscopn  23180  icccmplem2  23428  iccpnfcnv  23549  xrhmeo  23551  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  cmetcaulem  23892  ovolicc1  24120  ioorcl  24181  i1f1lem  24293  itg11  24295  itg1addlem2  24301  itg1addlem4  24303  i1fres  24309  itg1climres  24318  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1flim  24327  itg2const2  24345  itg2seq  24346  itg2uba  24347  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2cnlem1  24365  itg2cnlem2  24366  iblcnlem  24392  iblss  24408  iblss2  24409  itgitg2  24410  itgle  24413  itgss  24415  itgss2  24416  itgss3  24418  itgless  24420  ibladdlem  24423  itgaddlem1  24426  iblabslem  24431  iblabs  24432  iblabsr  24433  iblmulc2  24434  bddmulibl  24442  bddiblnc  24445  itggt0  24447  itgcn  24448  limcvallem  24474  ellimc2  24480  limccnp  24494  limccnp2  24495  limcco  24496  dvcobr  24549  dvexp2  24557  elply2  24793  elplyd  24799  ply1termlem  24800  coe1termlem  24855  abelthlem9  25035  logtayl  25251  leibpilem2  25527  leibpi  25528  rlimcnp2  25552  efrlim  25555  igamz  25633  isnsqf  25720  mule1  25733  sqff1o  25767  muinv  25778  chtublem  25795  dchrelbasd  25823  bposlem1  25868  bposlem3  25870  bposlem5  25872  bposlem6  25873  lgsval2lem  25891  lgsneg  25905  lgsdilem  25908  lgsdir2  25914  lgsdir  25916  lgsdi  25918  lgsne0  25919  gausslemma2dlem1a  25949  2lgslem1c  25977  2lgslem3  25988  2lgs  25991  dchrvmasum2if  26081  dchrvmasumiflem1  26085  rpvmasum2  26096  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  padicabv  26214  ostth2lem4  26220  axlowdimlem15  26750  opvtxval  26796  opiedgval  26799  elimifd  30310  elim2if  30311  ifeq3da  30313  pmtridf1o  30786  fzto1stfv1  30793  resvid2  30952  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhom  31290  indval2  31383  ind1  31386  sigaclfu2  31490  ddeval1  31603  eulerpartlemb  31736  ballotlemsima  31883  ballotlemrv1  31888  signsw0glem  31933  signswmnd  31937  signswrid  31938  indispconn  32594  ex-sategoelel  32781  ex-sategoelelomsuc  32786  ex-sategoelel12  32787  mrsubvr  32871  dfrdg2  33153  dfrdg3  33154  noprefixmo  33315  nosupno  33316  nosupbday  33318  nosupbnd1  33327  nosupbnd2  33329  unisnif  33499  dfrdg4  33525  fnejoin2  33830  unbdqndv2lem2  33962  bj-xpima2sn  34394  finxpreclem1  34806  finxpreclem3  34810  matunitlindflem1  35053  poimirlem2  35059  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem24  35081  mblfinlem2  35095  mbfposadd  35104  itg2addnclem  35108  itg2gt0cn  35112  ibladdnclem  35113  itgaddnclem1  35115  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  itggt0cn  35127  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  areacirclem5  35149  areacirc  35150  fdc  35183  heiborlem4  35252  ac6s6  35610  cdleme27a  37663  cdleme31sn1  37677  cdleme31fv1  37687  cdlemk40t  38214  dihvalb  38533  metakunt5  39354  metakunt6  39355  metakunt10  39359  metakunt11  39360  metakunt20  39369  fsuppind  39456  dffltz  39615  pw2f1ocnv  39978  aomclem5  40002  kelac1  40007  mon1pid  40149  arearect  40165  areaquad  40166  clsk1indlem1  40748  refsum2cnlem1  41666  upbdrech2  41940  lptioo2  42273  lptioo1  42274  limsupmnfuzlem  42368  limsupre3uzlem  42377  limsup10exlem  42414  coskpi2  42508  cosknegpi  42511  cncfiooicclem1  42535  cncfiooiccre  42537  dvnxpaek  42584  dvnprodlem1  42588  dvnprodlem3  42590  itgioocnicc  42619  iblcncfioo  42620  volico  42625  sublevolico  42626  volioore  42632  voliooico  42634  voliccico  42641  dirkerper  42738  dirkertrigeq  42743  dirkercncflem2  42746  fourierdlem10  42759  fourierdlem32  42781  fourierdlem33  42782  fourierdlem37  42786  fourierdlem62  42810  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem93  42841  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  etransclem4  42880  etransclem15  42891  etransclem19  42895  etransclem20  42896  etransclem23  42899  etransclem24  42900  etransclem25  42901  etransclem27  42903  etransclem31  42907  etransclem32  42908  ioorrnopnxrlem  42948  nnfoctbdjlem  43094  isomenndlem  43169  ovn0val  43189  hoidmv0val  43222  hsphoidmvle2  43224  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1le  43233  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoilem1  43240  hspdifhsp  43255  hoidifhspdmvle  43259  hspmbllem1  43265  hspmbllem2  43266  hspmbl  43268  volico2  43280  ovnsubadd2lem  43284  ovolval4lem2  43289  ovolval5lem1  43291  afvfundmfveq  43694  dfatafv2iota  43766  dfatafv2eqfv  43817  prproropf1olem3  44022  prproropf1olem4  44023  linc1  44834  lincext3  44865  lindslinindsimp1  44866  el0ldep  44875  islindeps2  44892  itcoval0  45076  ackval0  45094