Theorem iffalse 3634

Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)

Assertion

Ref	Expression
iffalse	⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

Proof of Theorem iffalse

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-if 3625	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 979	. . 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:  iffalsei  3635  iffalsed  3636  ifnefalse  3637  ifsbdc  3639  ifcldadc  3656  ifeq1dadc  3657  ifeqdadc  3659  ifbothdadc  3660  ifbothdc  3661  ifiddc  3662  ifcldcd  3664  ifnotdc  3665  2if2dc  3666  ifandc  3667  ifordc  3668  ifnetruedc  3670  pw2f1odclem  7100  fidifsnen  7138  nnnninf  7430  uzin  9905  modifeq2int  10772  seqf1oglem1  10905  seqf1oglem2  10906  bcval  11136  bcval3  11138  swrdccat  11452  pfxccat3a  11455  swrdccat3b  11457  sumrbdclem  12088  fsum3cvg  12089  summodclem2a  12092  sumsplitdc  12143  prodrbdclem  12282  fproddccvg  12283  prodssdc  12300  flodddiv4  12647  gcdn0val  12682  dfgcd2  12735  lcmn0val  12788  pcgcd  13052  pcmptcl  13065  pcmpt  13066  pcmpt2  13067  pcprod  13069  fldivp1  13071  unct  13277  lgsneg  16009  lgsdilem  16012  lgsdir2  16018  lgsdir  16020  lgsdi  16022  lgsne0  16023  gausslemma2dlem1a  16043  2lgslem1c  16075  2lgs  16089