This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dedhb

Description: A deduction theorem for converting the inference |- F/_ x A => |- ph into a closed theorem. Use nfa1 and nfab to eliminate the hypothesis of the substitution instance ps of the inference. For converting the inference form into a deduction form, abidnf is useful. (Contributed by NM, 8-Dec-2006)

	Ref	Expression
Hypotheses	dedhb.1	⊢ ( 𝐴 = { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } → ( 𝜑 ↔ 𝜓 ) )
	dedhb.2	⊢ 𝜓
Assertion	dedhb	⊢ ( Ⅎ 𝑥 𝐴 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dedhb.1	⊢ ( 𝐴 = { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } → ( 𝜑 ↔ 𝜓 ) )
2		dedhb.2	⊢ 𝜓
3		abidnf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )
4	3	eqcomd	⊢ ( Ⅎ 𝑥 𝐴 → 𝐴 = { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } )
5	4 1	syl	⊢ ( Ⅎ 𝑥 𝐴 → ( 𝜑 ↔ 𝜓 ) )
6	2 5	mpbiri	⊢ ( Ⅎ 𝑥 𝐴 → 𝜑 )