Theorem iftrue 4487

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ifcif 4481

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  iftruei  4488  iftrued  4489  iftrueb  4494  ifsb  4495  ifbi  4504  ifeq2da  4514  ifeq12da  4515  ifclda  4517  ifeqda  4518  elimif  4519  ifbothda  4520  ifid  4522  ifeqor  4533  ifnot  4534  ifan  4535  ifor  4536  2if2  4537  dedth  4540  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  dfopif  4828  dfopg  4829  somin1  6098  somincom  6099  xpima1  6149  elimdelov  7464  brif1  7465  ovif12  7468  ifmpt2v  7470  tz7.44-1  8347  rdg0n  8375  resixpfo  8886  boxriin  8890  boxcutc  8891  pw2f1olem  9021  unxpdomlem2  9169  unxpdomlem3  9170  infsupprpr  9421  ordtypelem1  9435  wemaplem2  9464  unwdomg  9501  ixpiunwdom  9507  cantnfp1lem2  9600  cantnfp1lem3  9601  ssttrcl  9636  ttrclselem2  9647  acndom  9973  dfac12lem2  10067  fin23lem14  10255  axcc2lem  10358  pwfseqlem2  10582  uzin  12799  xrmax1  13102  xrmax2  13103  xrmin1  13104  xrmin2  13105  max1ALT  13113  max0sub  13123  ifle  13124  xmulneg1  13196  fzprval  13513  fztpval  13514  modifeq2int  13868  seqf1olem1  13976  seqf1olem2  13977  bcval2  14240  tpf1ofv0  14431  tpf1ofv1  14432  ccatval1  14512  ccatalpha  14529  swrdccat  14670  pfxccat3a  14673  swrdccat3b  14675  repswswrd  14719  cshword  14726  0csh0  14728  ccatco  14770  sgnn  15029  max0add  15245  absmax  15265  sumrblem  15646  fsumcvg  15647  summolem2a  15650  isum  15654  sumss  15659  sumss2  15661  fsumcvg2  15662  fsumser  15665  fsumsplit  15676  sumsplit  15703  prodrblem  15864  fprodcvg  15865  prodmolem2a  15869  zprod  15872  iprod  15873  iprodn0  15875  prodss  15882  fprodsplit  15901  ruclem2  16169  ruclem3  16170  flodddiv4  16354  sadadd2lem2  16389  sadcf  16392  sadc0  16393  sadcp1  16394  sadcaddlem  16396  smupf  16417  smup0  16418  gcd0val  16436  dfgcd2  16485  eucalgf  16522  eucalginv  16523  eucalglt  16524  lcmf0val  16561  phisum  16730  pc0  16794  pcgcd  16818  pcmptcl  16831  pcmpt  16832  pcmpt2  16833  pcprod  16835  fldivp1  16837  prmreclem2  16857  prmreclem4  16859  1arithlem4  16866  vdwlem6  16926  ramtcl2  16951  ramcl2  16956  ramub1lem1  16966  prmop1  16978  fvprmselelfz  16984  fvprmselgcd1  16985  ressid2  17173  xpsfrnel  17495  xpsaddlem  17506  xpsvsca  17510  mreexexd  17583  gsumval1  18620  mgm2nsgrplem2  18856  sgrp2nmndlem2  18861  symgextfve  19360  symgfixfolem1  19379  pmtrmvd  19397  pmtrfinv  19402  pmtrprfval  19428  pmtrprfvalrn  19429  frgpuptinv  19712  frgpup2  19717  frgpup3lem  19718  cyggex  19839  gsumzsplit  19868  gsummpt1n0  19906  dprdfid  19960  dmdprdsplitlem  19980  sdrgacs  20746  abvtrivd  20777  znf1o  21518  uvcvv1  21756  psrlidm  21929  psrridm  21930  mvrf1  21953  mplmonmul  22003  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  mplmon2  22028  subrgasclcl  22034  evlslem3  22047  evlslem1  22049  psdmul  22121  psdmvr  22124  coe1tmfv1  22228  ply1sclid  22242  dmatmul  22453  scmatscmiddistr  22464  1mavmul  22504  mulmarep1gsum2  22530  1marepvmarrepid  22531  mdetdiag  22555  mdetralt2  22565  mdetunilem2  22569  mdetunilem7  22574  mdetunilem8  22575  mdetunilem9  22576  mndifsplit  22592  maducoeval2  22596  madugsum  22599  madurid  22600  gsummatr01lem3  22613  gsummatr01  22615  smadiadetglem2  22628  1elcpmat  22671  decpmatid  22726  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  ptpjpre1  23527  ptbasfi  23537  ptpjopn  23568  isfcls  23965  ptcmplem2  24009  ptcmplem3  24010  tsmssplit  24108  dscmet  24528  dscopn  24529  icccmplem2  24780  iccpnfcnv  24910  xrhmeo  24912  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  cmetcaulem  25256  ovolicc1  25485  ioorcl  25546  i1f1lem  25658  itg11  25660  itg1addlem2  25666  itg1addlem4  25668  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1flim  25692  itg2const2  25710  itg2seq  25711  itg2uba  25712  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2cnlem1  25730  itg2cnlem2  25731  iblcnlem  25758  iblss  25774  iblss2  25775  itgitg2  25776  itgle  25779  itgss  25781  itgss2  25782  itgss3  25784  itgless  25786  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblabsr  25799  iblmulc2  25800  bddmulibl  25808  bddiblnc  25811  itggt0  25813  itgcn  25814  limcvallem  25840  ellimc2  25846  limccnp  25860  limccnp2  25861  limcco  25862  dvcobr  25917  dvcobrOLD  25918  dvexp2  25926  mon1pid  26127  elply2  26169  elplyd  26175  ply1termlem  26176  coe1termlem  26231  abelthlem9  26418  logtayl  26637  leibpilem2  26919  leibpi  26920  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  igamz  27026  isnsqf  27113  mule1  27126  sqff1o  27160  muinv  27171  chtublem  27190  dchrelbasd  27218  bposlem1  27263  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgsval2lem  27286  lgsneg  27300  lgsdilem  27303  lgsdir2  27309  lgsdir  27311  lgsdi  27313  lgsne0  27314  gausslemma2dlem1a  27344  2lgslem1c  27372  2lgslem3  27383  2lgs  27386  dchrvmasum2if  27476  dchrvmasumiflem1  27480  rpvmasum2  27491  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  padicabv  27609  ostth2lem4  27615  nosupno  27683  nosupbday  27685  nosupbnd1  27694  nosupbnd2  27696  noinfno  27698  noinfbday  27700  noinfbnd1  27709  maxs1  27749  maxs2  27750  mins1  27751  mins2  27752  abssid  28249  abssge0  28253  axlowdimlem15  29041  opvtxval  29088  opiedgval  29091  elimifd  32629  elim2if  32630  ifeq3da  32632  ifnefals  32634  fmptunsnop  32789  indval2  32943  ind1  32946  pmtridf1o  33187  fzto1stfv1  33194  resvid2  33422  psrmonmul  33726  vieta  33756  2sqr3minply  33957  cos9thpiminply  33965  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  sigaclfu2  34298  ddeval1  34411  eulerpartlemb  34545  ballotlemsima  34693  ballotlemrv1  34698  signsw0glem  34730  signswmnd  34734  signswrid  34735  indispconn  35447  ex-sategoelel  35634  ex-sategoelelomsuc  35639  ex-sategoelel12  35640  mrsubvr  35724  dfrdg2  36006  dfrdg3  36007  unisnif  36136  dfrdg4  36164  fnejoin2  36582  unbdqndv2lem2  36729  bj-xpima2sn  37197  finxpreclem1  37633  finxpreclem3  37637  matunitlindflem1  37856  poimirlem2  37862  poimirlem15  37875  poimirlem16  37876  poimirlem17  37877  poimirlem19  37879  poimirlem20  37880  poimirlem24  37884  mblfinlem2  37898  mbfposadd  37907  itg2addnclem  37911  itg2gt0cn  37915  ibladdnclem  37916  itgaddnclem1  37918  iblabsnclem  37923  iblabsnc  37924  iblmulc2nc  37925  itggt0cn  37930  ftc1anclem4  37936  ftc1anclem5  37937  ftc1anclem6  37938  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941  areacirclem5  37952  areacirc  37953  fdc  37985  heiborlem4  38054  ac6s6  38412  cdleme27a  40732  cdleme31sn1  40746  cdleme31fv1  40756  cdlemk40t  41283  dihvalb  41602  sticksstones12a  42516  brif2  42585  brif12  42586  evlsbagval  42916  selvvvval  42932  fsuppind  42937  dffltz  42981  pw2f1ocnv  43383  aomclem5  43404  kelac1  43409  arearect  43561  areaquad  43562  oe0rif  43631  cantnfresb  43670  safesnsupfidom1o  43762  safesnsupfilb  43763  clsk1indlem1  44390  refsum2cnlem1  45386  upbdrech2  45659  lptioo2  45980  lptioo1  45981  limsupmnfuzlem  46073  limsupre3uzlem  46082  limsup10exlem  46119  coskpi2  46213  cosknegpi  46216  cncfiooicclem1  46240  cncfiooiccre  46242  dvnxpaek  46289  dvnprodlem1  46293  dvnprodlem3  46295  itgioocnicc  46324  iblcncfioo  46325  volico  46330  sublevolico  46331  volioore  46337  voliooico  46339  voliccico  46346  dirkerper  46443  dirkertrigeq  46448  dirkercncflem2  46451  fourierdlem10  46464  fourierdlem32  46486  fourierdlem33  46487  fourierdlem37  46491  fourierdlem62  46515  fourierdlem73  46526  fourierdlem74  46527  fourierdlem75  46528  fourierdlem79  46532  fourierdlem81  46534  fourierdlem82  46535  fourierdlem93  46546  fourierdlem97  46550  fourierdlem101  46554  fourierdlem103  46556  fourierdlem104  46557  sqwvfoura  46575  sqwvfourb  46576  fourierswlem  46577  fouriersw  46578  etransclem4  46585  etransclem15  46596  etransclem19  46600  etransclem20  46601  etransclem23  46604  etransclem24  46605  etransclem25  46606  etransclem27  46608  etransclem31  46612  etransclem32  46613  ioorrnopnxrlem  46653  nnfoctbdjlem  46802  isomenndlem  46877  ovn0val  46897  hoidmv0val  46930  hsphoidmvle2  46932  hoidmv1lelem1  46938  hoidmv1lelem2  46939  hoidmv1le  46941  hoidmvlelem2  46943  hoidmvlelem3  46944  ovnhoilem1  46948  hspdifhsp  46963  hoidifhspdmvle  46967  hspmbllem1  46973  hspmbllem2  46974  hspmbl  46976  volico2  46988  ovnsubadd2lem  46992  ovolval4lem2  46997  ovolval5lem1  46999  afvfundmfveq  47487  dfatafv2iota  47559  dfatafv2eqfv  47610  difmodm1lt  47708  prproropf1olem3  47854  prproropf1olem4  47855  linc1  48774  lincext3  48805  lindslinindsimp1  48806  el0ldep  48815  islindeps2  48832  itcoval0  49011  ackval0  49029