Theorem iftrue 3631

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 3625	. 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 3624

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 3625

This theorem is referenced by:  iftruei  3632  iftrued  3633  ifsbdc  3639  ifcldadc  3656  ifeqdadc  3659  ifbothdadc  3660  ifbothdc  3661  ifiddc  3662  ifcldcd  3664  ifnotdc  3665  2if2dc  3666  ifandc  3667  ifordc  3668  ifnefals  3671  pw2f1odclem  7100  fidifsnen  7138  nnnninf  7430  nnnninf2  7431  mkvprop  7462  iftrueb01  7546  uzin  9908  fzprval  10441  fztpval  10442  modifeq2int  10775  seqf1oglem1  10908  seqf1oglem2  10909  bcval  11139  bcval2  11140  ccatval1  11313  ccatalpha  11329  swrdccat  11455  pfxccat3a  11458  swrdccat3b  11460  sumrbdclem  12091  fsum3cvg  12092  summodclem2a  12095  isumss2  12107  fsum3ser  12111  fsumsplit  12121  sumsplitdc  12146  prodrbdclem  12285  fproddccvg  12286  iprodap  12294  iprodap0  12296  prodssdc  12303  fprodsplitdc  12310  flodddiv4  12650  gcd0val  12684  dfgcd2  12738  eucalgf  12780  eucalginv  12781  eucalglt  12782  phisum  12966  pc0  13030  pcgcd  13055  pcmptcl  13068  pcmpt  13069  pcmpt2  13070  pcprod  13072  fldivp1  13074  1arithlem4  13092  ballotfilemsima  13206  ballotfilemrv1  13211  unct  13280  xpsfrnel  13611  znf1o  14928  dvexp2  15706  elply2  15729  elplyd  15735  ply1termlem  15736  lgsval2lem  16012  lgsneg  16026  lgsdilem  16029  lgsdir2  16035  lgsdir  16037  lgsdi  16039  lgsne0  16040  gausslemma2dlem1a  16060  2lgslem1c  16092  2lgslem3  16103  2lgs  16106  opvtxval  16145  opiedgval  16148  depindlem1  16630  nnsf  16922  nninfsellemsuc  16929