Theorem iftrue 4092

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 1000	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))))
2	1	abbi2dv 2742	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))})
3		dfif2 4088	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))}
4	2, 3	syl6reqr 2675	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {cab 2608  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  iftruei  4093  iftrued  4094  ifsb  4099  ifbi  4107  ifeq2da  4117  ifeq12da  4118  ifclda  4120  ifeqda  4121  elimif  4122  ifbothda  4123  ifid  4125  ifeqor  4132  ifnot  4133  ifan  4134  ifor  4135  2if2  4136  dedth  4139  elimhyp  4146  elimhyp2v  4147  elimhyp3v  4148  elimhyp4v  4149  elimdhyp  4151  keephyp2v  4153  keephyp3v  4154  dfopif  4399  dfopg  4400  somin1  5529  somincom  5530  xpima1  5577  dfiota4OLD  5880  elimdelov  6736  ovif12  6739  tz7.44-1  7502  resixpfo  7946  boxriin  7950  boxcutc  7951  pw2f1olem  8064  unxpdomlem2  8165  unxpdomlem3  8166  ordtypelem1  8423  wemaplem2  8452  unwdomg  8489  ixpiunwdom  8496  cantnfp1lem2  8576  cantnfp1lem3  8577  acndom  8874  dfac12lem2  8966  fin23lem14  9155  axcc2lem  9258  pwfseqlem2  9481  uzin  11720  xrmax1  12006  xrmax2  12007  xrmin1  12008  xrmin2  12009  max1ALT  12017  max0sub  12027  ifle  12028  xmulneg1  12099  fzprval  12401  fztpval  12402  modifeq2int  12732  seqf1olem1  12840  seqf1olem2  12841  bcval2  13092  ccatval1  13361  ccatalpha  13375  swrdccat  13493  swrdccat3a  13494  swrdccat3b  13496  repswswrd  13531  cshword  13537  0csh0  13539  ccatco  13581  sgnn  13834  max0add  14050  absmax  14069  sumrblem  14442  fsumcvg  14443  summolem2a  14446  isum  14450  sumss  14455  sumss2  14457  fsumcvg2  14458  fsumser  14461  fsumsplit  14471  sumsplit  14499  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  zprod  14667  iprod  14668  iprodn0  14670  prodss  14677  fprodsplit  14696  ruclem2  14961  ruclem3  14962  flodddiv4  15137  sadadd2lem2  15172  sadcf  15175  sadc0  15176  sadcp1  15177  sadcaddlem  15179  smupf  15200  smup0  15201  gcd0val  15219  dfgcd2  15263  eucalgf  15296  eucalginv  15297  eucalglt  15298  lcmf0val  15335  phisum  15495  pc0  15559  pcgcd  15582  pcmptcl  15595  pcmpt  15596  pcmpt2  15597  pcprod  15599  fldivp1  15601  prmreclem2  15621  prmreclem4  15623  1arithlem4  15630  vdwlem6  15690  ramtcl2  15715  ramcl2  15720  ramub1lem1  15730  prmop1  15742  fvprmselelfz  15748  fvprmselgcd1  15749  ressid2  15928  xpscfv  16222  xpsfrnel  16223  xpsaddlem  16235  xpsvsca  16239  mreexexd  16308  gsumval1  17277  mgm2nsgrplem2  17406  sgrp2nmndlem2  17411  symgextfve  17839  symgfixfolem1  17858  pmtrmvd  17876  pmtrfinv  17881  pmtrprfval  17907  pmtrprfvalrn  17908  frgpuptinv  18184  frgpup2  18189  frgpup3lem  18190  cyggex  18299  gsumzsplit  18327  gsummpt1n0  18364  dprdfid  18416  dmdprdsplitlem  18436  abvtrivd  18840  psrlidm  19403  psrridm  19404  mvrf1  19425  mplmonmul  19464  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  mplmon2  19493  subrgasclcl  19499  evlslem3  19514  evlslem1  19515  coe1tmfv1  19644  ply1sclid  19658  znf1o  19900  uvcvv1  20128  dmatmul  20303  scmatscmiddistr  20314  1mavmul  20354  mulmarep1gsum2  20380  1marepvmarrepid  20381  mdetdiag  20405  mdetralt2  20415  mdetunilem2  20419  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  mndifsplit  20442  maducoeval2  20446  madugsum  20449  madurid  20450  gsummatr01lem3  20463  gsummatr01  20465  smadiadetglem2  20478  1elcpmat  20520  decpmatid  20575  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  ptpjpre1  21374  ptbasfi  21384  ptpjopn  21415  isfcls  21813  ptcmplem2  21857  ptcmplem3  21858  tsmssplit  21955  dscmet  22377  dscopn  22378  icccmplem2  22626  iccpnfcnv  22743  xrhmeo  22745  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  cmetcaulem  23086  ovolicc1  23284  ioorcl  23345  i1f1lem  23456  itg11  23458  itg1addlem2  23464  itg1addlem4  23466  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1flim  23490  itg2const2  23508  itg2seq  23509  itg2uba  23510  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2cnlem1  23528  itg2cnlem2  23529  iblcnlem  23555  iblss  23571  iblss2  23572  itgitg2  23573  itgle  23576  itgss  23578  itgss2  23579  itgss3  23581  itgless  23583  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  bddmulibl  23605  itggt0  23608  itgcn  23609  limcvallem  23635  ellimc2  23641  limccnp  23655  limccnp2  23656  limcco  23657  dvcobr  23709  dvexp2  23717  elply2  23952  elplyd  23958  ply1termlem  23959  coe1termlem  24014  abelthlem9  24194  logtayl  24406  leibpilem2  24668  leibpi  24669  rlimcnp2  24693  efrlim  24696  igamz  24774  isnsqf  24861  mule1  24874  sqff1o  24908  muinv  24919  chtublem  24936  dchrelbasd  24964  bposlem1  25009  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgsval2lem  25032  lgsneg  25046  lgsdilem  25049  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsne0  25060  gausslemma2dlem1a  25090  2lgslem1c  25118  2lgslem3  25129  2lgs  25132  dchrvmasum2if  25186  dchrvmasumiflem1  25190  rpvmasum2  25201  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  padicabv  25319  ostth2lem4  25325  axlowdimlem15  25836  opvtxval  25883  opiedgval  25886  elimifd  29362  elim2if  29363  ifeq3da  29365  resvid2  29828  fzto1stfv1  29851  pmtridf1o  29856  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  indval2  30076  ind1  30079  sigaclfu2  30184  ddeval1  30297  eulerpartlemb  30430  ballotlemsima  30577  ballotlemrv1  30582  signsw0glem  30630  signswmnd  30634  signswrid  30635  indispconn  31216  mrsubvr  31408  dfrdg2  31701  dfrdg3  31702  noprefixmo  31848  nosupno  31849  nosupbday  31851  nosupbnd1  31860  nosupbnd2  31862  unisnif  32032  dfrdg4  32058  fnejoin2  32364  unbdqndv2lem2  32501  bj-xpima2sn  32945  finxpreclem1  33226  finxpreclem3  33230  matunitlindflem1  33405  poimirlem2  33411  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  mblfinlem2  33447  mbfposadd  33457  itg2addnclem  33461  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  itggt0cn  33482  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem5  33504  areacirc  33505  fdc  33541  heiborlem4  33613  ac6s6  33980  cdleme27a  35655  cdleme31sn1  35669  cdleme31fv1  35679  cdlemk40t  36206  dihvalb  36526  pw2f1ocnv  37604  aomclem5  37628  kelac1  37633  sdrgacs  37771  mon1pid  37783  arearect  37801  areaquad  37802  clsk1indlem1  38343  refsum2cnlem1  39196  upbdrech2  39522  lptioo2  39863  lptioo1  39864  limsupmnfuzlem  39958  limsupre3uzlem  39967  limsup10exlem  40004  coskpi2  40077  cosknegpi  40080  cncfiooicclem1  40106  cncfiooiccre  40108  dvnxpaek  40157  dvnprodlem1  40161  dvnprodlem3  40163  itgioocnicc  40193  iblcncfioo  40194  volico  40200  sublevolico  40201  volioore  40207  voliooico  40209  voliccico  40216  dirkerper  40313  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem10  40334  fourierdlem32  40356  fourierdlem33  40357  fourierdlem37  40361  fourierdlem62  40385  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem93  40416  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem4  40455  etransclem15  40466  etransclem19  40470  etransclem20  40471  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem27  40478  etransclem31  40482  etransclem32  40483  ioorrnopnxrlem  40526  nnfoctbdjlem  40672  isomenndlem  40744  ovn0val  40764  hoidmv0val  40797  hsphoidmvle2  40799  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem1  40815  hspdifhsp  40830  hoidifhspdmvle  40834  hspmbllem1  40840  hspmbllem2  40841  hspmbl  40843  volico2  40855  ovnsubadd2lem  40859  ovolval4lem2  40864  ovolval5lem1  40866  afvfundmfveq  41218  pfxccat3a  41429  cshword2  41437  linc1  42214  lincext3  42245  lindslinindsimp1  42246  el0ldep  42255  islindeps2  42272