Theorem ifhvhv0 30984

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

Syntax hints:   ∈ wcel 2109  ifcif 4478   ℋchba 30881  0_ℎc0v 30886

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 2701  ax-hv0cl 30965

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  hvsubsub4  31022  hvnegdi  31029  hvsubeq0  31030  hvaddcan  31032  hvsubadd  31039  normlem9at  31083  normsq  31096  normsub0  31098  norm-ii  31100  norm-iii  31102  normsub  31105  normpyth  31107  norm3dif  31112  norm3lemt  31114  norm3adifi  31115  normpar  31117  polid  31121  bcs  31143  pjoc1  31396  pjoc2  31401  h1de2ci  31518  spansn  31521  elspansn  31528  elspansn2  31529  h1datom  31544  spansnj  31609  spansncv  31615  pjch1  31632  pjadji  31647  pjaddi  31648  pjinormi  31649  pjsubi  31650  pjmuli  31651  pjcjt2  31654  pjch  31656  pjopyth  31682  pjnorm  31686  pjpyth  31687  pjnel  31688  eigre  31797  eigorth  31800  lnopeq0lem2  31968  lnopunii  31974  lnophmi  31980  pjss2coi  32126  pjssmi  32127  pjssge0i  32128  pjdifnormi  32129