Theorem ifhvhv0 31109

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

Syntax hints:   ∈ wcel 2114  ifcif 4481   ℋchba 31006  0_ℎc0v 31011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-hv0cl 31090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  hvsubsub4  31147  hvnegdi  31154  hvsubeq0  31155  hvaddcan  31157  hvsubadd  31164  normlem9at  31208  normsq  31221  normsub0  31223  norm-ii  31225  norm-iii  31227  normsub  31230  normpyth  31232  norm3dif  31237  norm3lemt  31239  norm3adifi  31240  normpar  31242  polid  31246  bcs  31268  pjoc1  31521  pjoc2  31526  h1de2ci  31643  spansn  31646  elspansn  31653  elspansn2  31654  h1datom  31669  spansnj  31734  spansncv  31740  pjch1  31757  pjadji  31772  pjaddi  31773  pjinormi  31774  pjsubi  31775  pjmuli  31776  pjcjt2  31779  pjch  31781  pjopyth  31807  pjnorm  31811  pjpyth  31812  pjnel  31813  eigre  31922  eigorth  31925  lnopeq0lem2  32093  lnopunii  32099  lnophmi  32105  pjss2coi  32251  pjssmi  32252  pjssge0i  32253  pjdifnormi  32254