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

Metamath Proof Explorer

Theorem cbv3hv

Description: Rule used to change bound variables, using implicit substitution. Version of cbv3h with a disjoint variable condition on x , y , which does not require ax-13 . Was used in a proof of axc11n (but of independent interest). (Contributed by NM, 25-Jul-2015) (Proof shortened by Wolf Lammen, 29-Nov-2020) (Proof shortened by BJ, 30-Nov-2020)

	Ref	Expression
Hypotheses	cbv3hv.nf1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
	cbv3hv.nf2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
	cbv3hv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
Assertion	cbv3hv	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbv3hv.nf1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
2		cbv3hv.nf2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3		cbv3hv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
4	1	nf5i	⊢ Ⅎ 𝑦 𝜑
5	2	nf5i	⊢ Ⅎ 𝑥 𝜓
6	4 5 3	cbv3v	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 )