Theorem iffalse 3629

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716   = wceq 1398   ∈ wcel 2203  {cab 2218  ifcif 3619

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3620

This theorem is referenced by:  iffalsei  3630  iffalsed  3631  ifnefalse  3632  ifsbdc  3634  ifcldadc  3651  ifeq1dadc  3652  ifeqdadc  3654  ifbothdadc  3655  ifbothdc  3656  ifiddc  3657  ifcldcd  3659  ifnotdc  3660  2if2dc  3661  ifandc  3662  ifordc  3663  ifnetruedc  3665  pw2f1odclem  7086  fidifsnen  7124  nnnninf  7416  uzin  9886  modifeq2int  10747  seqf1oglem1  10880  seqf1oglem2  10881  bcval  11110  bcval3  11112  swrdccat  11423  pfxccat3a  11426  swrdccat3b  11428  sumrbdclem  12059  fsum3cvg  12060  summodclem2a  12063  sumsplitdc  12114  prodrbdclem  12253  fproddccvg  12254  prodssdc  12271  flodddiv4  12618  gcdn0val  12653  dfgcd2  12706  lcmn0val  12759  pcgcd  13023  pcmptcl  13036  pcmpt  13037  pcmpt2  13038  pcprod  13040  fldivp1  13042  unct  13185  lgsneg  15889  lgsdilem  15892  lgsdir2  15898  lgsdir  15900  lgsdi  15902  lgsne0  15903  gausslemma2dlem1a  15923  2lgslem1c  15955  2lgs  15969