Theorem ifhvhv0 30275

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

Syntax hints:   ∈ wcel 2107  ifcif 4529   ℋchba 30172  0_ℎc0v 30177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-hv0cl 30256

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  hvsubsub4  30313  hvnegdi  30320  hvsubeq0  30321  hvaddcan  30323  hvsubadd  30330  normlem9at  30374  normsq  30387  normsub0  30389  norm-ii  30391  norm-iii  30393  normsub  30396  normpyth  30398  norm3dif  30403  norm3lemt  30405  norm3adifi  30406  normpar  30408  polid  30412  bcs  30434  pjoc1  30687  pjoc2  30692  h1de2ci  30809  spansn  30812  elspansn  30819  elspansn2  30820  h1datom  30835  spansnj  30900  spansncv  30906  pjch1  30923  pjadji  30938  pjaddi  30939  pjinormi  30940  pjsubi  30941  pjmuli  30942  pjcjt2  30945  pjch  30947  pjopyth  30973  pjnorm  30977  pjpyth  30978  pjnel  30979  eigre  31088  eigorth  31091  lnopeq0lem2  31259  lnopunii  31265  lnophmi  31271  pjss2coi  31417  pjssmi  31418  pjssge0i  31419  pjdifnormi  31420