Theorem iffalse 3648

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 3639	. 2 ⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
2		dedlemb 983	. . 3 ⊢ (¬ 𝜑 → (𝑥 ∈ 𝐵 ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))))
3	2	abbi2dv 2359	. 2 ⊢ (¬ 𝜑 → 𝐵 = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))})
4	1, 3	eqtr4id 2290	1 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720   = wceq 1402   ∈ wcel 2209  {cab 2224  ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  iffalsei  3649  iffalsed  3650  ifnefalse  3651  ifsbdc  3653  ifcldadc  3670  ifeq1dadc  3671  ifeqdadc  3673  ifbothdadc  3674  ifbothdc  3675  ifiddc  3676  ifcldcd  3678  ifnotdc  3679  2if2dc  3680  ifandc  3681  ifordc  3682  ifnetruedc  3684  pw2f1odclem  7134  fidifsnen  7172  nnnninf  7467  uzin  9965  modifeq2int  10837  seqf1oglem1  10970  seqf1oglem2  10971  bcval  11202  bcval3  11204  swrdccat  11522  pfxccat3a  11525  swrdccat3b  11527  sumrbdclem  12162  fsum3cvg  12163  summodclem2a  12166  sumsplitdc  12217  prodrbdclem  12356  fproddccvg  12357  prodssdc  12374  flodddiv4  12721  gcdn0val  12756  dfgcd2  12809  lcmn0val  12862  pcgcd  13130  pcmptcl  13143  pcmpt  13144  pcmpt2  13145  pcprod  13147  fldivp1  13149  unct  13384  chtublem  16217  bposlem1  16233  bposlem3  16235  bposlem5  16237  lgsneg  16265  lgsdilem  16268  lgsdir2  16274  lgsdir  16276  lgsdi  16278  lgsne0  16279  gausslemma2dlem1a  16299  2lgslem1c  16331  2lgs  16345