Theorem iffalse 3570

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 3563	. 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 3562

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 3563

This theorem is referenced by:  iffalsei  3571  iffalsed  3572  ifnefalse  3573  ifsbdc  3574  ifcldadc  3591  ifeq1dadc  3592  ifbothdadc  3594  ifbothdc  3595  ifiddc  3596  ifcldcd  3598  ifnotdc  3599  ifandc  3600  ifordc  3601  ifnetruedc  3603  pw2f1odclem  6904  fidifsnen  6940  nnnninf  7201  uzin  9653  modifeq2int  10497  seqf1oglem1  10630  seqf1oglem2  10631  bcval  10860  bcval3  10862  sumrbdclem  11561  fsum3cvg  11562  summodclem2a  11565  sumsplitdc  11616  prodrbdclem  11755  fproddccvg  11756  prodssdc  11773  flodddiv4  12120  gcdn0val  12155  dfgcd2  12208  lcmn0val  12261  pcgcd  12525  pcmptcl  12538  pcmpt  12539  pcmpt2  12540  pcprod  12542  fldivp1  12544  unct  12686  lgsneg  15373  lgsdilem  15376  lgsdir2  15382  lgsdir  15384  lgsdi  15386  lgsne0  15387  gausslemma2dlem1a  15407  2lgslem1c  15439  2lgs  15453