Theorem iftrue 3607

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 3603	. 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 3602

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 3603

This theorem is referenced by:  iftruei  3608  iftrued  3609  ifsbdc  3615  ifcldadc  3632  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  ifcldcd  3640  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  ifnefals  3647  pw2f1odclem  7003  fidifsnen  7040  nnnninf  7301  nnnninf2  7302  mkvprop  7333  iftrueb01  7416  uzin  9763  fzprval  10286  fztpval  10287  modifeq2int  10616  seqf1oglem1  10749  seqf1oglem2  10750  bcval  10979  bcval2  10980  ccatval1  11140  swrdccat  11275  pfxccat3a  11278  swrdccat3b  11280  sumrbdclem  11896  fsum3cvg  11897  summodclem2a  11900  isumss2  11912  fsum3ser  11916  fsumsplit  11926  sumsplitdc  11951  prodrbdclem  12090  fproddccvg  12091  iprodap  12099  iprodap0  12101  prodssdc  12108  fprodsplitdc  12115  flodddiv4  12455  gcd0val  12489  dfgcd2  12543  eucalgf  12585  eucalginv  12586  eucalglt  12587  phisum  12771  pc0  12835  pcgcd  12860  pcmptcl  12873  pcmpt  12874  pcmpt2  12875  pcprod  12877  fldivp1  12879  1arithlem4  12897  unct  13021  xpsfrnel  13385  znf1o  14623  dvexp2  15394  elply2  15417  elplyd  15423  ply1termlem  15424  lgsval2lem  15697  lgsneg  15711  lgsdilem  15714  lgsdir2  15720  lgsdir  15722  lgsdi  15724  lgsne0  15725  gausslemma2dlem1a  15745  2lgslem1c  15777  2lgslem3  15788  2lgs  15791  opvtxval  15830  opiedgval  15833  nnsf  16401  nninfsellemsuc  16408