Theorem ifhvhv0 28805

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 28786	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4492	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 2111  ifcif 4425   ℋchba 28702  0_ℎc0v 28707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-hv0cl 28786

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  hvsubsub4  28843  hvnegdi  28850  hvsubeq0  28851  hvaddcan  28853  hvsubadd  28860  normlem9at  28904  normsq  28917  normsub0  28919  norm-ii  28921  norm-iii  28923  normsub  28926  normpyth  28928  norm3dif  28933  norm3lemt  28935  norm3adifi  28936  normpar  28938  polid  28942  bcs  28964  pjoc1  29217  pjoc2  29222  h1de2ci  29339  spansn  29342  elspansn  29349  elspansn2  29350  h1datom  29365  spansnj  29430  spansncv  29436  pjch1  29453  pjadji  29468  pjaddi  29469  pjinormi  29470  pjsubi  29471  pjmuli  29472  pjcjt2  29475  pjch  29477  pjopyth  29503  pjnorm  29507  pjpyth  29508  pjnel  29509  eigre  29618  eigorth  29621  lnopeq0lem2  29789  lnopunii  29795  lnophmi  29801  pjss2coi  29947  pjssmi  29948  pjssge0i  29949  pjdifnormi  29950