Theorem ifhvhv0 31340

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

Syntax hints:   ∈ wcel 2141  ifcif 4486   ℋchba 31237  0_ℎc0v 31242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-hv0cl 31321

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487

This theorem is referenced by:  hvsubsub4  31378  hvnegdi  31385  hvsubeq0  31386  hvaddcan  31388  hvsubadd  31395  normlem9at  31439  normsq  31452  normsub0  31454  norm-ii  31456  norm-iii  31458  normsub  31461  normpyth  31463  norm3dif  31468  norm3lemt  31470  norm3adifi  31471  normpar  31473  polid  31477  bcs  31499  pjoc1  31752  pjoc2  31757  h1de2ci  31874  spansn  31877  elspansn  31884  elspansn2  31885  h1datom  31900  spansnj  31965  spansncv  31971  pjch1  31988  pjadji  32003  pjaddi  32004  pjinormi  32005  pjsubi  32006  pjmuli  32007  pjcjt2  32010  pjch  32012  pjopyth  32038  pjnorm  32042  pjpyth  32043  pjnel  32044  eigre  32153  eigorth  32156  lnopeq0lem2  32324  lnopunii  32330  lnophmi  32336  pjss2coi  32482  pjssmi  32483  pjssge0i  32484  pjdifnormi  32485