Theorem ifhvhv0 31080

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

Syntax hints:   ∈ wcel 2114  ifcif 4480   ℋchba 30977  0_ℎc0v 30982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-hv0cl 31061

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4481

This theorem is referenced by:  hvsubsub4  31118  hvnegdi  31125  hvsubeq0  31126  hvaddcan  31128  hvsubadd  31135  normlem9at  31179  normsq  31192  normsub0  31194  norm-ii  31196  norm-iii  31198  normsub  31201  normpyth  31203  norm3dif  31208  norm3lemt  31210  norm3adifi  31211  normpar  31213  polid  31217  bcs  31239  pjoc1  31492  pjoc2  31497  h1de2ci  31614  spansn  31617  elspansn  31624  elspansn2  31625  h1datom  31640  spansnj  31705  spansncv  31711  pjch1  31728  pjadji  31743  pjaddi  31744  pjinormi  31745  pjsubi  31746  pjmuli  31747  pjcjt2  31750  pjch  31752  pjopyth  31778  pjnorm  31782  pjpyth  31783  pjnel  31784  eigre  31893  eigorth  31896  lnopeq0lem2  32064  lnopunii  32070  lnophmi  32076  pjss2coi  32222  pjssmi  32223  pjssge0i  32224  pjdifnormi  32225