Theorem ifhvhv0 31385

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

This proof depends on syntax axioms:   ∈ wcel 2142  ifcif 4486   ℋchba 31282  0_ℎc0v 31287

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-hv0cl 31366

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4487

This theorem is used by:  hvsubsub4  31423  hvnegdi  31430  hvsubeq0  31431  hvaddcan  31433  hvsubadd  31440  normlem9at  31484  normsq  31497  normsub0  31499  norm-ii  31501  norm-iii  31503  normsub  31506  normpyth  31508  norm3dif  31513  norm3lemt  31515  norm3adifi  31516  normpar  31518  polid  31522  bcs  31544  pjoc1  31797  pjoc2  31802  h1de2ci  31919  spansn  31922  elspansn  31929  elspansn2  31930  h1datom  31945  spansnj  32010  spansncv  32016  pjch1  32033  pjadji  32048  pjaddi  32049  pjinormi  32050  pjsubi  32051  pjmuli  32052  pjcjt2  32055  pjch  32057  pjopyth  32083  pjnorm  32087  pjpyth  32088  pjnel  32089  eigre  32198  eigorth  32201  lnopeq0lem2  32369  lnopunii  32375  lnophmi  32381  pjss2coi  32527  pjssmi  32528  pjssge0i  32529  pjdifnormi  32530