Theorem ifhvhv0 31041

Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0_ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)

Assertion

Ref	Expression
ifhvhv0	⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Proof of Theorem ifhvhv0

Step	Hyp	Ref	Expression
1		ax-hv0cl 31022	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4595	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 2108  ifcif 4525   ℋchba 30938  0_ℎc0v 30943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-hv0cl 31022

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  hvsubsub4  31079  hvnegdi  31086  hvsubeq0  31087  hvaddcan  31089  hvsubadd  31096  normlem9at  31140  normsq  31153  normsub0  31155  norm-ii  31157  norm-iii  31159  normsub  31162  normpyth  31164  norm3dif  31169  norm3lemt  31171  norm3adifi  31172  normpar  31174  polid  31178  bcs  31200  pjoc1  31453  pjoc2  31458  h1de2ci  31575  spansn  31578  elspansn  31585  elspansn2  31586  h1datom  31601  spansnj  31666  spansncv  31672  pjch1  31689  pjadji  31704  pjaddi  31705  pjinormi  31706  pjsubi  31707  pjmuli  31708  pjcjt2  31711  pjch  31713  pjopyth  31739  pjnorm  31743  pjpyth  31744  pjnel  31745  eigre  31854  eigorth  31857  lnopeq0lem2  32025  lnopunii  32031  lnophmi  32037  pjss2coi  32183  pjssmi  32184  pjssge0i  32185  pjdifnormi  32186