Theorem iftrue 3629

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 3623	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlema 978	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	abbi2dv 2355	. 2 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2286	1 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716   = wceq 1398   ∈ wcel 2205  {cab 2220  ifcif 3622

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3623

This theorem is referenced by:  iftruei  3630  iftrued  3631  ifsbdc  3637  ifcldadc  3654  ifeqdadc  3657  ifbothdadc  3658  ifbothdc  3659  ifiddc  3660  ifcldcd  3662  ifnotdc  3663  2if2dc  3664  ifandc  3665  ifordc  3666  ifnefals  3669  pw2f1odclem  7089  fidifsnen  7127  nnnninf  7419  nnnninf2  7420  mkvprop  7451  iftrueb01  7535  uzin  9893  fzprval  10423  fztpval  10424  modifeq2int  10755  seqf1oglem1  10888  seqf1oglem2  10889  bcval  11119  bcval2  11120  ccatval1  11293  ccatalpha  11309  swrdccat  11435  pfxccat3a  11438  swrdccat3b  11440  sumrbdclem  12071  fsum3cvg  12072  summodclem2a  12075  isumss2  12087  fsum3ser  12091  fsumsplit  12101  sumsplitdc  12126  prodrbdclem  12265  fproddccvg  12266  iprodap  12274  iprodap0  12276  prodssdc  12283  fprodsplitdc  12290  flodddiv4  12630  gcd0val  12664  dfgcd2  12718  eucalgf  12760  eucalginv  12761  eucalglt  12762  phisum  12946  pc0  13010  pcgcd  13035  pcmptcl  13048  pcmpt  13049  pcmpt2  13050  pcprod  13052  fldivp1  13054  1arithlem4  13072  unct  13214  xpsfrnel  13578  znf1o  14848  dvexp2  15626  elply2  15649  elplyd  15655  ply1termlem  15656  lgsval2lem  15932  lgsneg  15946  lgsdilem  15949  lgsdir2  15955  lgsdir  15957  lgsdi  15959  lgsne0  15960  gausslemma2dlem1a  15980  2lgslem1c  16012  2lgslem3  16023  2lgs  16026  opvtxval  16065  opiedgval  16068  depindlem1  16550  nnsf  16832  nninfsellemsuc  16839