Theorem ifhvhv0 31118

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

Syntax hints:   ∈ wcel 2119  ifcif 4461   ℋchba 31015  0_ℎc0v 31020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-hv0cl 31099

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  hvsubsub4  31156  hvnegdi  31163  hvsubeq0  31164  hvaddcan  31166  hvsubadd  31173  normlem9at  31217  normsq  31230  normsub0  31232  norm-ii  31234  norm-iii  31236  normsub  31239  normpyth  31241  norm3dif  31246  norm3lemt  31248  norm3adifi  31249  normpar  31251  polid  31255  bcs  31277  pjoc1  31530  pjoc2  31535  h1de2ci  31652  spansn  31655  elspansn  31662  elspansn2  31663  h1datom  31678  spansnj  31743  spansncv  31749  pjch1  31766  pjadji  31781  pjaddi  31782  pjinormi  31783  pjsubi  31784  pjmuli  31785  pjcjt2  31788  pjch  31790  pjopyth  31816  pjnorm  31820  pjpyth  31821  pjnel  31822  eigre  31931  eigorth  31934  lnopeq0lem2  32102  lnopunii  32108  lnophmi  32114  pjss2coi  32260  pjssmi  32261  pjssge0i  32262  pjdifnormi  32263