Theorem iftrue 3608

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		df-if 3604	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlema 975	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	abbi2dv 2348	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2281	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713   = wceq 1395   ∈ wcel 2200  {cab 2215  ifcif 3603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3604

This theorem is referenced by:  iftruei  3609  iftrued  3610  ifsbdc  3616  ifcldadc  3633  ifeqdadc  3636  ifbothdadc  3637  ifbothdc  3638  ifiddc  3639  ifcldcd  3641  ifnotdc  3642  2if2dc  3643  ifandc  3644  ifordc  3645  ifnefals  3648  pw2f1odclem  7015  fidifsnen  7052  nnnninf  7319  nnnninf2  7320  mkvprop  7351  iftrueb01  7434  uzin  9782  fzprval  10310  fztpval  10311  modifeq2int  10641  seqf1oglem1  10774  seqf1oglem2  10775  bcval  11004  bcval2  11005  ccatval1  11167  ccatalpha  11183  swrdccat  11309  pfxccat3a  11312  swrdccat3b  11314  sumrbdclem  11931  fsum3cvg  11932  summodclem2a  11935  isumss2  11947  fsum3ser  11951  fsumsplit  11961  sumsplitdc  11986  prodrbdclem  12125  fproddccvg  12126  iprodap  12134  iprodap0  12136  prodssdc  12143  fprodsplitdc  12150  flodddiv4  12490  gcd0val  12524  dfgcd2  12578  eucalgf  12620  eucalginv  12621  eucalglt  12622  phisum  12806  pc0  12870  pcgcd  12895  pcmptcl  12908  pcmpt  12909  pcmpt2  12910  pcprod  12912  fldivp1  12914  1arithlem4  12932  unct  13056  xpsfrnel  13420  znf1o  14658  dvexp2  15429  elply2  15452  elplyd  15458  ply1termlem  15459  lgsval2lem  15732  lgsneg  15746  lgsdilem  15749  lgsdir2  15755  lgsdir  15757  lgsdi  15759  lgsne0  15760  gausslemma2dlem1a  15780  2lgslem1c  15812  2lgslem3  15823  2lgs  15826  opvtxval  15865  opiedgval  15868  nnsf  16557  nninfsellemsuc  16564