Theorem ifhvhv0 31009

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

Syntax hints:   ∈ wcel 2111  ifcif 4474   ℋchba 30906  0_ℎc0v 30911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-hv0cl 30990

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4475

This theorem is referenced by:  hvsubsub4  31047  hvnegdi  31054  hvsubeq0  31055  hvaddcan  31057  hvsubadd  31064  normlem9at  31108  normsq  31121  normsub0  31123  norm-ii  31125  norm-iii  31127  normsub  31130  normpyth  31132  norm3dif  31137  norm3lemt  31139  norm3adifi  31140  normpar  31142  polid  31146  bcs  31168  pjoc1  31421  pjoc2  31426  h1de2ci  31543  spansn  31546  elspansn  31553  elspansn2  31554  h1datom  31569  spansnj  31634  spansncv  31640  pjch1  31657  pjadji  31672  pjaddi  31673  pjinormi  31674  pjsubi  31675  pjmuli  31676  pjcjt2  31679  pjch  31681  pjopyth  31707  pjnorm  31711  pjpyth  31712  pjnel  31713  eigre  31822  eigorth  31825  lnopeq0lem2  31993  lnopunii  31999  lnophmi  32005  pjss2coi  32151  pjssmi  32152  pjssge0i  32153  pjdifnormi  32154