Theorem ifhvhv0 31625

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

This proof depends on syntax axioms:   ∈ wcel 2144  ifcif 4481   ℋchba 31522  0_ℎc0v 31527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-hv0cl 31606

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  hvsubsub4  31663  hvnegdi  31670  hvsubeq0  31671  hvaddcan  31673  hvsubadd  31680  normlem9at  31724  normsq  31737  normsub0  31739  norm-ii  31741  norm-iii  31743  normsub  31746  normpyth  31748  norm3dif  31753  norm3lemt  31755  norm3adifi  31756  normpar  31758  polid  31762  bcs  31784  pjoc1  32037  pjoc2  32042  h1de2ci  32159  spansn  32162  elspansn  32169  elspansn2  32170  h1datom  32185  spansnj  32250  spansncv  32256  pjch1  32273  pjadji  32288  pjaddi  32289  pjinormi  32290  pjsubi  32291  pjmuli  32292  pjcjt2  32295  pjch  32297  pjopyth  32323  pjnorm  32327  pjpyth  32328  pjnel  32329  eigre  32438  eigorth  32441  lnopeq0lem2  32609  lnopunii  32615  lnophmi  32621  pjss2coi  32767  pjssmi  32768  pjssge0i  32769  pjdifnormi  32770