Theorem ifhvhv0 29393

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

Syntax hints:   ∈ wcel 2107  ifcif 4460   ℋchba 29290  0_ℎc0v 29295

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 2710  ax-hv0cl 29374

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461

This theorem is referenced by:  hvsubsub4  29431  hvnegdi  29438  hvsubeq0  29439  hvaddcan  29441  hvsubadd  29448  normlem9at  29492  normsq  29505  normsub0  29507  norm-ii  29509  norm-iii  29511  normsub  29514  normpyth  29516  norm3dif  29521  norm3lemt  29523  norm3adifi  29524  normpar  29526  polid  29530  bcs  29552  pjoc1  29805  pjoc2  29810  h1de2ci  29927  spansn  29930  elspansn  29937  elspansn2  29938  h1datom  29953  spansnj  30018  spansncv  30024  pjch1  30041  pjadji  30056  pjaddi  30057  pjinormi  30058  pjsubi  30059  pjmuli  30060  pjcjt2  30063  pjch  30065  pjopyth  30091  pjnorm  30095  pjpyth  30096  pjnel  30097  eigre  30206  eigorth  30209  lnopeq0lem2  30377  lnopunii  30383  lnophmi  30389  pjss2coi  30535  pjssmi  30536  pjssge0i  30537  pjdifnormi  30538