Theorem ifhvhv0 30530

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

Syntax hints:   ∈ wcel 2106  ifcif 4528   ℋchba 30427  0_ℎc0v 30432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-hv0cl 30511

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  hvsubsub4  30568  hvnegdi  30575  hvsubeq0  30576  hvaddcan  30578  hvsubadd  30585  normlem9at  30629  normsq  30642  normsub0  30644  norm-ii  30646  norm-iii  30648  normsub  30651  normpyth  30653  norm3dif  30658  norm3lemt  30660  norm3adifi  30661  normpar  30663  polid  30667  bcs  30689  pjoc1  30942  pjoc2  30947  h1de2ci  31064  spansn  31067  elspansn  31074  elspansn2  31075  h1datom  31090  spansnj  31155  spansncv  31161  pjch1  31178  pjadji  31193  pjaddi  31194  pjinormi  31195  pjsubi  31196  pjmuli  31197  pjcjt2  31200  pjch  31202  pjopyth  31228  pjnorm  31232  pjpyth  31233  pjnel  31234  eigre  31343  eigorth  31346  lnopeq0lem2  31514  lnopunii  31520  lnophmi  31526  pjss2coi  31672  pjssmi  31673  pjssge0i  31674  pjdifnormi  31675