Theorem iffalse 3610

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713   = wceq 1395   ∈ wcel 2200  {cab 2215  ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  iffalsei  3611  iffalsed  3612  ifnefalse  3613  ifsbdc  3615  ifcldadc  3632  ifeq1dadc  3633  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  ifcldcd  3640  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  ifnetruedc  3646  pw2f1odclem  6983  fidifsnen  7020  nnnninf  7281  uzin  9743  modifeq2int  10595  seqf1oglem1  10728  seqf1oglem2  10729  bcval  10958  bcval3  10960  swrdccat  11253  pfxccat3a  11256  swrdccat3b  11258  sumrbdclem  11874  fsum3cvg  11875  summodclem2a  11878  sumsplitdc  11929  prodrbdclem  12068  fproddccvg  12069  prodssdc  12086  flodddiv4  12433  gcdn0val  12468  dfgcd2  12521  lcmn0val  12574  pcgcd  12838  pcmptcl  12851  pcmpt  12852  pcmpt2  12853  pcprod  12855  fldivp1  12857  unct  12999  lgsneg  15688  lgsdilem  15691  lgsdir2  15697  lgsdir  15699  lgsdi  15701  lgsne0  15702  gausslemma2dlem1a  15722  2lgslem1c  15754  2lgs  15768