Theorem iftrue 4467

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2718  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  iftruei  4468  iftrued  4469  iftrueb  4474  ifsb  4475  ifbi  4484  ifeq2da  4494  ifeq12da  4495  ifclda  4497  ifeqda  4498  elimif  4499  ifbothda  4500  ifid  4502  ifeqor  4513  ifnot  4514  ifan  4515  ifor  4516  2if2  4517  dedth  4520  elimhyp  4527  elimhyp2v  4528  elimhyp3v  4529  elimhyp4v  4530  elimdhyp  4532  keephyp2v  4534  keephyp3v  4535  dfopif  4808  dfopg  4809  somin1  6090  somincom  6091  xpima1  6141  elimdelov  7459  brif1  7460  ovif12  7463  ifmpt2v  7465  tz7.44-1  8342  rdg0n  8370  resixpfo  8881  boxriin  8885  boxcutc  8886  pw2f1olem  9016  unxpdomlem2  9164  unxpdomlem3  9165  infsupprpr  9416  ordtypelem1  9430  wemaplem2  9459  unwdomg  9496  ixpiunwdom  9502  cantnfp1lem2  9598  cantnfp1lem3  9599  ssttrcl  9634  ttrclselem2  9645  acndom  9971  dfac12lem2  10065  fin23lem14  10253  axcc2lem  10356  pwfseqlem2  10580  indval2  12162  ind1  12166  uzin  12822  xrmax1  13125  xrmax2  13126  xrmin1  13127  xrmin2  13128  max1ALT  13136  max0sub  13146  ifle  13147  xmulneg1  13219  fzprval  13537  fztpval  13538  modifeq2int  13893  seqf1olem1  14001  seqf1olem2  14002  bcval2  14265  tpf1ofv0  14456  tpf1ofv1  14457  ccatval1  14537  ccatalpha  14554  swrdccat  14695  pfxccat3a  14698  swrdccat3b  14700  repswswrd  14744  cshword  14751  0csh0  14753  ccatco  14795  sgnn  15054  max0add  15270  absmax  15290  sumrblem  15671  fsumcvg  15672  summolem2a  15675  isum  15679  sumss  15684  sumss2  15686  fsumcvg2  15687  fsumser  15690  fsumsplit  15701  sumsplit  15728  prodrblem  15892  fprodcvg  15893  prodmolem2a  15897  zprod  15900  iprod  15901  iprodn0  15903  prodss  15910  fprodsplit  15929  ruclem2  16197  ruclem3  16198  flodddiv4  16382  sadadd2lem2  16417  sadcf  16420  sadc0  16421  sadcp1  16422  sadcaddlem  16424  smupf  16445  smup0  16446  gcd0val  16464  dfgcd2  16513  eucalgf  16550  eucalginv  16551  eucalglt  16552  lcmf0val  16589  phisum  16759  pc0  16823  pcgcd  16847  pcmptcl  16860  pcmpt  16861  pcmpt2  16862  pcprod  16864  fldivp1  16866  prmreclem2  16886  prmreclem4  16888  1arithlem4  16895  vdwlem6  16955  ramtcl2  16980  ramcl2  16985  ramub1lem1  16995  prmop1  17007  fvprmselelfz  17013  fvprmselgcd1  17014  ressid2  17202  xpsfrnel  17524  xpsaddlem  17535  xpsvsca  17539  mreexexd  17612  gsumval1  18649  mgm2nsgrplem2  18888  sgrp2nmndlem2  18893  symgextfve  19392  symgfixfolem1  19411  pmtrmvd  19429  pmtrfinv  19434  pmtrprfval  19460  pmtrprfvalrn  19461  frgpuptinv  19744  frgpup2  19749  frgpup3lem  19750  cyggex  19871  gsumzsplit  19900  gsummpt1n0  19938  dprdfid  19992  dmdprdsplitlem  20012  sdrgacs  20780  abvtrivd  20811  znf1o  21533  uvcvv1  21771  psrlidm  21943  psrridm  21944  mvrf1  21967  mplmonmul  22019  mplcoe1  22020  mplcoe3  22021  mplcoe5  22023  mplmon2  22044  subrgasclcl  22050  evlslem3  22063  evlslem1  22065  selvvvval  22125  psdmul  22161  psdmvr  22164  coe1tmfv1  22267  ply1sclid  22281  dmatmul  22487  scmatscmiddistr  22498  1mavmul  22538  mulmarep1gsum2  22564  1marepvmarrepid  22565  mdetdiag  22589  mdetralt2  22599  mdetunilem2  22603  mdetunilem7  22608  mdetunilem8  22609  mdetunilem9  22610  mndifsplit  22626  maducoeval2  22630  madugsum  22633  madurid  22634  gsummatr01lem3  22647  gsummatr01  22649  smadiadetglem2  22662  1elcpmat  22705  decpmatid  22760  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  ptpjpre1  23561  ptbasfi  23571  ptpjopn  23602  isfcls  23999  ptcmplem2  24043  ptcmplem3  24044  tsmssplit  24142  dscmet  24562  dscopn  24563  icccmplem2  24814  iccpnfcnv  24936  xrhmeo  24938  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  cmetcaulem  25280  ovolicc1  25508  ioorcl  25569  i1f1lem  25681  itg11  25683  itg1addlem2  25689  itg1addlem4  25691  i1fres  25697  itg1climres  25706  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1flim  25715  itg2const2  25733  itg2seq  25734  itg2uba  25735  itg2splitlem  25740  itg2split  25741  itg2monolem1  25742  itg2cnlem1  25753  itg2cnlem2  25754  iblcnlem  25781  iblss  25797  iblss2  25798  itgitg2  25799  itgle  25802  itgss  25804  itgss2  25805  itgss3  25807  itgless  25809  ibladdlem  25812  itgaddlem1  25815  iblabslem  25820  iblabs  25821  iblabsr  25822  iblmulc2  25823  bddmulibl  25831  bddiblnc  25834  itggt0  25836  itgcn  25837  limcvallem  25863  ellimc2  25869  limccnp  25883  limccnp2  25884  limcco  25885  dvcobr  25938  dvexp2  25946  mon1pid  26144  elply2  26186  elplyd  26192  ply1termlem  26193  coe1termlem  26248  abelthlem9  26430  logtayl  26649  leibpilem2  26930  leibpi  26931  rlimcnp2  26955  efrlim  26958  igamz  27036  isnsqf  27123  mule1  27136  sqff1o  27170  muinv  27181  chtublem  27199  dchrelbasd  27227  bposlem1  27272  bposlem3  27274  bposlem5  27276  bposlem6  27277  lgsval2lem  27295  lgsneg  27309  lgsdilem  27312  lgsdir2  27318  lgsdir  27320  lgsdi  27322  lgsne0  27323  gausslemma2dlem1a  27353  2lgslem1c  27381  2lgslem3  27392  2lgs  27395  dchrvmasum2if  27485  dchrvmasumiflem1  27489  rpvmasum2  27500  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  padicabv  27618  ostth2lem4  27624  nosupno  27692  nosupbday  27694  nosupbnd1  27703  nosupbnd2  27705  noinfno  27707  noinfbday  27709  noinfbnd1  27718  maxs1  27758  maxs2  27759  mins1  27760  mins2  27761  abssid  28258  abssge0  28262  axlowdimlem15  29050  opvtxval  29097  opiedgval  29100  elimifd  32638  elim2if  32639  ifeq3da  32641  ifnefals  32643  fmptunsnop  32799  pmtridf1o  33182  fzto1stfv1  33189  resvid2  33420  psrmonmul  33741  vieta  33771  2sqr3minply  33971  cos9thpiminply  33979  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  sigaclfu2  34312  ddeval1  34425  eulerpartlemb  34559  ballotlemsima  34707  ballotlemrv1  34712  signsw0glem  34744  signswmnd  34748  signswrid  34749  indispconn  35463  ex-sategoelel  35650  ex-sategoelelomsuc  35655  ex-sategoelel12  35656  mrsubvr  35740  dfrdg2  36022  dfrdg3  36023  unisnif  36152  dfrdg4  36180  fnejoin2  36598  unbdqndv2lem2  36817  bj-xpima2sn  37312  finxpreclem1  37752  finxpreclem3  37756  matunitlindflem1  37984  poimirlem2  37990  poimirlem15  38003  poimirlem16  38004  poimirlem17  38005  poimirlem19  38007  poimirlem20  38008  poimirlem24  38012  mblfinlem2  38026  mbfposadd  38035  itg2addnclem  38039  itg2gt0cn  38043  ibladdnclem  38044  itgaddnclem1  38046  iblabsnclem  38051  iblabsnc  38052  iblmulc2nc  38053  itggt0cn  38058  ftc1anclem4  38064  ftc1anclem5  38065  ftc1anclem6  38066  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069  areacirclem5  38080  areacirc  38081  fdc  38113  heiborlem4  38182  ac6s6  38540  cdleme27a  40860  cdleme31sn1  40874  cdleme31fv1  40884  cdlemk40t  41411  dihvalb  41730  sticksstones12a  42643  brif2  42712  brif12  42713  evlsbagval  43037  fsuppind  43041  dffltz  43085  pw2f1ocnv  43483  aomclem5  43504  kelac1  43509  arearect  43661  areaquad  43662  oe0rif  43731  cantnfresb  43770  safesnsupfidom1o  43862  safesnsupfilb  43863  clsk1indlem1  44490  refsum2cnlem1  45486  upbdrech2  45757  lptioo2  46077  lptioo1  46078  limsupmnfuzlem  46170  limsupre3uzlem  46179  limsup10exlem  46216  coskpi2  46310  cosknegpi  46313  cncfiooicclem1  46337  cncfiooiccre  46339  dvnxpaek  46386  dvnprodlem1  46390  dvnprodlem3  46392  itgioocnicc  46421  iblcncfioo  46422  volico  46427  sublevolico  46428  volioore  46434  voliooico  46436  voliccico  46443  dirkerper  46540  dirkertrigeq  46545  dirkercncflem2  46548  fourierdlem10  46561  fourierdlem32  46583  fourierdlem33  46584  fourierdlem37  46588  fourierdlem62  46612  fourierdlem73  46623  fourierdlem74  46624  fourierdlem75  46625  fourierdlem79  46629  fourierdlem81  46631  fourierdlem82  46632  fourierdlem93  46643  fourierdlem97  46647  fourierdlem101  46651  fourierdlem103  46653  fourierdlem104  46654  sqwvfoura  46672  sqwvfourb  46673  fourierswlem  46674  fouriersw  46675  etransclem4  46682  etransclem15  46693  etransclem19  46697  etransclem20  46698  etransclem23  46701  etransclem24  46702  etransclem25  46703  etransclem27  46705  etransclem31  46709  etransclem32  46710  ioorrnopnxrlem  46750  nnfoctbdjlem  46899  isomenndlem  46974  ovn0val  46994  hoidmv0val  47027  hsphoidmvle2  47029  hoidmv1lelem1  47035  hoidmv1lelem2  47036  hoidmv1le  47038  hoidmvlelem2  47040  hoidmvlelem3  47041  ovnhoilem1  47045  hspdifhsp  47060  hoidifhspdmvle  47064  hspmbllem1  47070  hspmbllem2  47071  hspmbl  47073  volico2  47085  ovnsubadd2lem  47089  ovolval4lem2  47094  ovolval5lem1  47096  afvfundmfveq  47602  dfatafv2iota  47674  dfatafv2eqfv  47725  difmodm1lt  47829  prproropf1olem3  47981  prproropf1olem4  47982  linc1  48917  lincext3  48948  lindslinindsimp1  48949  el0ldep  48958  islindeps2  48975  itcoval0  49154  ackval0  49172