Theorem ifhvhv0 31315

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

Syntax hints:   ∈ wcel 2149  ifcif 4492   ℋchba 31212  0_ℎc0v 31217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-hv0cl 31296

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  hvsubsub4  31353  hvnegdi  31360  hvsubeq0  31361  hvaddcan  31363  hvsubadd  31370  normlem9at  31414  normsq  31427  normsub0  31429  norm-ii  31431  norm-iii  31433  normsub  31436  normpyth  31438  norm3dif  31443  norm3lemt  31445  norm3adifi  31446  normpar  31448  polid  31452  bcs  31474  pjoc1  31727  pjoc2  31732  h1de2ci  31849  spansn  31852  elspansn  31859  elspansn2  31860  h1datom  31875  spansnj  31940  spansncv  31946  pjch1  31963  pjadji  31978  pjaddi  31979  pjinormi  31980  pjsubi  31981  pjmuli  31982  pjcjt2  31985  pjch  31987  pjopyth  32013  pjnorm  32017  pjpyth  32018  pjnel  32019  eigre  32128  eigorth  32131  lnopeq0lem2  32299  lnopunii  32305  lnophmi  32311  pjss2coi  32457  pjssmi  32458  pjssge0i  32459  pjdifnormi  32460