Theorem ifhvhv0 28969

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

Syntax hints:   ∈ wcel 2114  ifcif 4424   ℋchba 28866  0_ℎc0v 28871

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-hv0cl 28950

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-if 4425

This theorem is referenced by:  hvsubsub4  29007  hvnegdi  29014  hvsubeq0  29015  hvaddcan  29017  hvsubadd  29024  normlem9at  29068  normsq  29081  normsub0  29083  norm-ii  29085  norm-iii  29087  normsub  29090  normpyth  29092  norm3dif  29097  norm3lemt  29099  norm3adifi  29100  normpar  29102  polid  29106  bcs  29128  pjoc1  29381  pjoc2  29386  h1de2ci  29503  spansn  29506  elspansn  29513  elspansn2  29514  h1datom  29529  spansnj  29594  spansncv  29600  pjch1  29617  pjadji  29632  pjaddi  29633  pjinormi  29634  pjsubi  29635  pjmuli  29636  pjcjt2  29639  pjch  29641  pjopyth  29667  pjnorm  29671  pjpyth  29672  pjnel  29673  eigre  29782  eigorth  29785  lnopeq0lem2  29953  lnopunii  29959  lnophmi  29965  pjss2coi  30111  pjssmi  30112  pjssge0i  30113  pjdifnormi  30114