Theorem elimf 6709

Description: Eliminate a mapping hypothesis for the weak deduction theorem dedth 4540, when a special case 𝐺:𝐴⟶𝐵 is provable, in order to convert 𝐹:𝐴⟶𝐵 from a hypothesis to an antecedent. (Contributed by NM, 24-Aug-2006.)

Hypothesis

Ref	Expression
elimf.1	⊢ 𝐺:𝐴⟶𝐵

Assertion

Ref	Expression
elimf	⊢ if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺):𝐴⟶𝐵

Proof of Theorem elimf

Step	Hyp	Ref	Expression
1		feq1 6688	. 2 ⊢ (𝐹 = if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺) → (𝐹:𝐴⟶𝐵 ↔ if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺):𝐴⟶𝐵))
2		feq1 6688	. 2 ⊢ (𝐺 = if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺) → (𝐺:𝐴⟶𝐵 ↔ if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺):𝐴⟶𝐵))
3		elimf.1	. 2 ⊢ 𝐺:𝐴⟶𝐵
4	1, 2, 3	elimhyp 4547	1 ⊢ if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺):𝐴⟶𝐵

This proof depends on syntax axioms:  ifcif 4481  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6541  df-fn 6542  df-f 6543

This theorem is used by:  hosubcl  32381  hoaddcom  32382  hoaddass  32390  hocsubdir  32393  hoaddrid  32399  hodid  32400  ho0sub  32405  honegsub  32407  hoddi  32598