Theorem ifhvhv0 31164

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

Syntax hints:   ∈ wcel 2136  ifcif 4474   ℋchba 31061  0_ℎc0v 31066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-hv0cl 31145

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-if 4475

This theorem is referenced by:  hvsubsub4  31202  hvnegdi  31209  hvsubeq0  31210  hvaddcan  31212  hvsubadd  31219  normlem9at  31263  normsq  31276  normsub0  31278  norm-ii  31280  norm-iii  31282  normsub  31285  normpyth  31287  norm3dif  31292  norm3lemt  31294  norm3adifi  31295  normpar  31297  polid  31301  bcs  31323  pjoc1  31576  pjoc2  31581  h1de2ci  31698  spansn  31701  elspansn  31708  elspansn2  31709  h1datom  31724  spansnj  31789  spansncv  31795  pjch1  31812  pjadji  31827  pjaddi  31828  pjinormi  31829  pjsubi  31830  pjmuli  31831  pjcjt2  31834  pjch  31836  pjopyth  31862  pjnorm  31866  pjpyth  31867  pjnel  31868  eigre  31977  eigorth  31980  lnopeq0lem2  32148  lnopunii  32154  lnophmi  32160  pjss2coi  32306  pjssmi  32307  pjssge0i  32308  pjdifnormi  32309