Theorem ifhvhv0 30992

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

Syntax hints:   ∈ wcel 2110  ifcif 4473   ℋchba 30889  0_ℎc0v 30894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-hv0cl 30973

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4474

This theorem is referenced by:  hvsubsub4  31030  hvnegdi  31037  hvsubeq0  31038  hvaddcan  31040  hvsubadd  31047  normlem9at  31091  normsq  31104  normsub0  31106  norm-ii  31108  norm-iii  31110  normsub  31113  normpyth  31115  norm3dif  31120  norm3lemt  31122  norm3adifi  31123  normpar  31125  polid  31129  bcs  31151  pjoc1  31404  pjoc2  31409  h1de2ci  31526  spansn  31529  elspansn  31536  elspansn2  31537  h1datom  31552  spansnj  31617  spansncv  31623  pjch1  31640  pjadji  31655  pjaddi  31656  pjinormi  31657  pjsubi  31658  pjmuli  31659  pjcjt2  31662  pjch  31664  pjopyth  31690  pjnorm  31694  pjpyth  31695  pjnel  31696  eigre  31805  eigorth  31808  lnopeq0lem2  31976  lnopunii  31982  lnophmi  31988  pjss2coi  32134  pjssmi  32135  pjssge0i  32136  pjdifnormi  32137