Theorem iffalse 3544

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 708   = wceq 1353   ∈ wcel 2148  {cab 2163  ifcif 3536

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3537

This theorem is referenced by:  iffalsei  3545  iffalsed  3546  ifnefalse  3547  ifsbdc  3548  ifcldadc  3565  ifeq1dadc  3566  ifbothdadc  3568  ifbothdc  3569  ifiddc  3570  ifcldcd  3572  ifnotdc  3573  ifandc  3574  ifordc  3575  fidifsnen  6872  nnnninf  7126  uzin  9562  modifeq2int  10388  bcval  10731  bcval3  10733  sumrbdclem  11387  fsum3cvg  11388  summodclem2a  11391  sumsplitdc  11442  prodrbdclem  11581  fproddccvg  11582  prodssdc  11599  flodddiv4  11941  gcdn0val  11964  dfgcd2  12017  lcmn0val  12068  pcgcd  12330  pcmptcl  12342  pcmpt  12343  pcmpt2  12344  pcprod  12346  fldivp1  12348  unct  12445  lgsneg  14510  lgsdilem  14513  lgsdir2  14519  lgsdir  14521  lgsdi  14523  lgsne0  14524