Theorem iffalse 3569

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 709   = wceq 1364   ∈ wcel 2167  {cab 2182  ifcif 3561

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 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3562

This theorem is referenced by:  iffalsei  3570  iffalsed  3571  ifnefalse  3572  ifsbdc  3573  ifcldadc  3590  ifeq1dadc  3591  ifbothdadc  3593  ifbothdc  3594  ifiddc  3595  ifcldcd  3597  ifnotdc  3598  ifandc  3599  ifordc  3600  ifnetruedc  3602  pw2f1odclem  6895  fidifsnen  6931  nnnninf  7192  uzin  9634  modifeq2int  10478  seqf1oglem1  10611  seqf1oglem2  10612  bcval  10841  bcval3  10843  sumrbdclem  11542  fsum3cvg  11543  summodclem2a  11546  sumsplitdc  11597  prodrbdclem  11736  fproddccvg  11737  prodssdc  11754  flodddiv4  12101  gcdn0val  12128  dfgcd2  12181  lcmn0val  12234  pcgcd  12498  pcmptcl  12511  pcmpt  12512  pcmpt2  12513  pcprod  12515  fldivp1  12517  unct  12659  lgsneg  15265  lgsdilem  15268  lgsdir2  15274  lgsdir  15276  lgsdi  15278  lgsne0  15279  gausslemma2dlem1a  15299  2lgslem1c  15331  2lgs  15345