Theorem ifhvhv0 28423

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

Syntax hints:   ∈ wcel 2164  ifcif 4306   ℋchba 28320  0_ℎc0v 28325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803  ax-hv0cl 28404

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-if 4307

This theorem is referenced by:  hvsubsub4  28461  hvnegdi  28468  hvsubeq0  28469  hvaddcan  28471  hvsubadd  28478  normlem9at  28522  normsq  28535  normsub0  28537  norm-ii  28539  norm-iii  28541  normsub  28544  normpyth  28546  norm3dif  28551  norm3lemt  28553  norm3adifi  28554  normpar  28556  polid  28560  bcs  28582  pjoc1  28837  pjoc2  28842  h1de2ci  28959  spansn  28962  elspansn  28969  elspansn2  28970  h1datom  28985  spansnj  29050  spansncv  29056  pjch1  29073  pjadji  29088  pjaddi  29089  pjinormi  29090  pjsubi  29091  pjmuli  29092  pjcjt2  29095  pjch  29097  pjopyth  29123  pjnorm  29127  pjpyth  29128  pjnel  29129  eigre  29238  eigorth  29241  lnopeq0lem2  29409  lnopunii  29415  lnophmi  29421  pjss2coi  29567  pjssmi  29568  pjssge0i  29569  pjdifnormi  29570