Theorem iftrue 3611

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 715   = wceq 1397   ∈ wcel 2201  {cab 2216  ifcif 3604

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-if 3605

This theorem is referenced by:  iftruei  3612  iftrued  3613  ifsbdc  3619  ifcldadc  3636  ifeqdadc  3639  ifbothdadc  3640  ifbothdc  3641  ifiddc  3642  ifcldcd  3644  ifnotdc  3645  2if2dc  3646  ifandc  3647  ifordc  3648  ifnefals  3651  pw2f1odclem  7025  fidifsnen  7062  nnnninf  7330  nnnninf2  7331  mkvprop  7362  iftrueb01  7446  uzin  9794  fzprval  10322  fztpval  10323  modifeq2int  10654  seqf1oglem1  10787  seqf1oglem2  10788  bcval  11017  bcval2  11018  ccatval1  11183  ccatalpha  11199  swrdccat  11325  pfxccat3a  11328  swrdccat3b  11330  sumrbdclem  11961  fsum3cvg  11962  summodclem2a  11965  isumss2  11977  fsum3ser  11981  fsumsplit  11991  sumsplitdc  12016  prodrbdclem  12155  fproddccvg  12156  iprodap  12164  iprodap0  12166  prodssdc  12173  fprodsplitdc  12180  flodddiv4  12520  gcd0val  12554  dfgcd2  12608  eucalgf  12650  eucalginv  12651  eucalglt  12652  phisum  12836  pc0  12900  pcgcd  12925  pcmptcl  12938  pcmpt  12939  pcmpt2  12940  pcprod  12942  fldivp1  12944  1arithlem4  12962  unct  13086  xpsfrnel  13450  znf1o  14689  dvexp2  15465  elply2  15488  elplyd  15494  ply1termlem  15495  lgsval2lem  15768  lgsneg  15782  lgsdilem  15785  lgsdir2  15791  lgsdir  15793  lgsdi  15795  lgsne0  15796  gausslemma2dlem1a  15816  2lgslem1c  15848  2lgslem3  15859  2lgs  15862  opvtxval  15901  opiedgval  15904  depindlem1  16386  nnsf  16670  nninfsellemsuc  16677