Theorem iftrue 3626

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716   = wceq 1398   ∈ wcel 2203  {cab 2218  ifcif 3619

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3620

This theorem is referenced by:  iftruei  3627  iftrued  3628  ifsbdc  3634  ifcldadc  3651  ifeqdadc  3654  ifbothdadc  3655  ifbothdc  3656  ifiddc  3657  ifcldcd  3659  ifnotdc  3660  2if2dc  3661  ifandc  3662  ifordc  3663  ifnefals  3666  pw2f1odclem  7086  fidifsnen  7124  nnnninf  7416  nnnninf2  7417  mkvprop  7448  iftrueb01  7532  uzin  9883  fzprval  10412  fztpval  10413  modifeq2int  10744  seqf1oglem1  10877  seqf1oglem2  10878  bcval  11107  bcval2  11108  ccatval1  11278  ccatalpha  11294  swrdccat  11420  pfxccat3a  11423  swrdccat3b  11425  sumrbdclem  12056  fsum3cvg  12057  summodclem2a  12060  isumss2  12072  fsum3ser  12076  fsumsplit  12086  sumsplitdc  12111  prodrbdclem  12250  fproddccvg  12251  iprodap  12259  iprodap0  12261  prodssdc  12268  fprodsplitdc  12275  flodddiv4  12615  gcd0val  12649  dfgcd2  12703  eucalgf  12745  eucalginv  12746  eucalglt  12747  phisum  12931  pc0  12995  pcgcd  13020  pcmptcl  13033  pcmpt  13034  pcmpt2  13035  pcprod  13037  fldivp1  13039  1arithlem4  13057  unct  13182  xpsfrnel  13546  znf1o  14786  dvexp2  15564  elply2  15587  elplyd  15593  ply1termlem  15594  lgsval2lem  15870  lgsneg  15884  lgsdilem  15887  lgsdir2  15893  lgsdir  15895  lgsdi  15897  lgsne0  15898  gausslemma2dlem1a  15918  2lgslem1c  15950  2lgslem3  15961  2lgs  15964  opvtxval  16003  opiedgval  16006  depindlem1  16488  nnsf  16770  nninfsellemsuc  16777