Theorem ifhvhv0 31051

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

Syntax hints:   ∈ wcel 2106  ifcif 4531   ℋchba 30948  0_ℎc0v 30953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-hv0cl 31032

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  hvsubsub4  31089  hvnegdi  31096  hvsubeq0  31097  hvaddcan  31099  hvsubadd  31106  normlem9at  31150  normsq  31163  normsub0  31165  norm-ii  31167  norm-iii  31169  normsub  31172  normpyth  31174  norm3dif  31179  norm3lemt  31181  norm3adifi  31182  normpar  31184  polid  31188  bcs  31210  pjoc1  31463  pjoc2  31468  h1de2ci  31585  spansn  31588  elspansn  31595  elspansn2  31596  h1datom  31611  spansnj  31676  spansncv  31682  pjch1  31699  pjadji  31714  pjaddi  31715  pjinormi  31716  pjsubi  31717  pjmuli  31718  pjcjt2  31721  pjch  31723  pjopyth  31749  pjnorm  31753  pjpyth  31754  pjnel  31755  eigre  31864  eigorth  31867  lnopeq0lem2  32035  lnopunii  32041  lnophmi  32047  pjss2coi  32193  pjssmi  32194  pjssge0i  32195  pjdifnormi  32196