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

Metamath Proof Explorer

Theorem bj-cbv2v

Description: Version of cbv2 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	bj-cbv2v.1	⊢ Ⅎ 𝑥 𝜑
		bj-cbv2v.2	⊢ Ⅎ 𝑦 𝜑
		bj-cbv2v.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
		bj-cbv2v.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
		bj-cbv2v.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
	Assertion	bj-cbv2v	⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbv2v.1	⊢ Ⅎ 𝑥 𝜑
2		bj-cbv2v.2	⊢ Ⅎ 𝑦 𝜑
3		bj-cbv2v.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
4		bj-cbv2v.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
5		bj-cbv2v.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
6	2	nf5ri	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
7	1	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜑
8	7	nf5ri	⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )
9	6 8	syl	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )
10	3	nf5rd	⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑦 𝜓 ) )
11	4	nf5rd	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜒 ) )
12	10 11 5	bj-cbv2hv	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )
13	9 12	syl	⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )