Theorem ifhvhv0 30958

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

Syntax hints:   ∈ wcel 2109  ifcif 4491   ℋchba 30855  0_ℎc0v 30860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-hv0cl 30939

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  hvsubsub4  30996  hvnegdi  31003  hvsubeq0  31004  hvaddcan  31006  hvsubadd  31013  normlem9at  31057  normsq  31070  normsub0  31072  norm-ii  31074  norm-iii  31076  normsub  31079  normpyth  31081  norm3dif  31086  norm3lemt  31088  norm3adifi  31089  normpar  31091  polid  31095  bcs  31117  pjoc1  31370  pjoc2  31375  h1de2ci  31492  spansn  31495  elspansn  31502  elspansn2  31503  h1datom  31518  spansnj  31583  spansncv  31589  pjch1  31606  pjadji  31621  pjaddi  31622  pjinormi  31623  pjsubi  31624  pjmuli  31625  pjcjt2  31628  pjch  31630  pjopyth  31656  pjnorm  31660  pjpyth  31661  pjnel  31662  eigre  31771  eigorth  31774  lnopeq0lem2  31942  lnopunii  31948  lnophmi  31954  pjss2coi  32100  pjssmi  32101  pjssge0i  32102  pjdifnormi  32103