Theorem ifhvhv0 30951

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

Syntax hints:   ∈ wcel 2109  ifcif 4488   ℋchba 30848  0_ℎc0v 30853

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-hv0cl 30932

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  hvsubsub4  30989  hvnegdi  30996  hvsubeq0  30997  hvaddcan  30999  hvsubadd  31006  normlem9at  31050  normsq  31063  normsub0  31065  norm-ii  31067  norm-iii  31069  normsub  31072  normpyth  31074  norm3dif  31079  norm3lemt  31081  norm3adifi  31082  normpar  31084  polid  31088  bcs  31110  pjoc1  31363  pjoc2  31368  h1de2ci  31485  spansn  31488  elspansn  31495  elspansn2  31496  h1datom  31511  spansnj  31576  spansncv  31582  pjch1  31599  pjadji  31614  pjaddi  31615  pjinormi  31616  pjsubi  31617  pjmuli  31618  pjcjt2  31621  pjch  31623  pjopyth  31649  pjnorm  31653  pjpyth  31654  pjnel  31655  eigre  31764  eigorth  31767  lnopeq0lem2  31935  lnopunii  31941  lnophmi  31947  pjss2coi  32093  pjssmi  32094  pjssge0i  32095  pjdifnormi  32096