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  7013  fidifsnen  7050  nnnninf  7314  nnnninf2  7315  mkvprop  7346  iftrueb01  7429  uzin  9777  fzprval  10305  fztpval  10306  modifeq2int  10636  seqf1oglem1  10769  seqf1oglem2  10770  bcval  10999  bcval2  11000  ccatval1  11161  ccatalpha  11177  swrdccat  11303  pfxccat3a  11306  swrdccat3b  11308  sumrbdclem  11925  fsum3cvg  11926  summodclem2a  11929  isumss2  11941  fsum3ser  11945  fsumsplit  11955  sumsplitdc  11980  prodrbdclem  12119  fproddccvg  12120  iprodap  12128  iprodap0  12130  prodssdc  12137  fprodsplitdc  12144  flodddiv4  12484  gcd0val  12518  dfgcd2  12572  eucalgf  12614  eucalginv  12615  eucalglt  12616  phisum  12800  pc0  12864  pcgcd  12889  pcmptcl  12902  pcmpt  12903  pcmpt2  12904  pcprod  12906  fldivp1  12908  1arithlem4  12926  unct  13050  xpsfrnel  13414  znf1o  14652  dvexp2  15423  elply2  15446  elplyd  15452  ply1termlem  15453  lgsval2lem  15726  lgsneg  15740  lgsdilem  15743  lgsdir2  15749  lgsdir  15751  lgsdi  15753  lgsne0  15754  gausslemma2dlem1a  15774  2lgslem1c  15806  2lgslem3  15817  2lgs  15820  opvtxval  15859  opiedgval  15862  nnsf  16517  nninfsellemsuc  16524