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

Metamath Proof Explorer

Theorem cbvex2v

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Sep-2003) (Revised by BJ, 16-Jun-2019)

		Ref	Expression
	Hypotheses	cbval2v.1	$⊢ Ⅎ z φ$
		cbval2v.2	$⊢ Ⅎ w φ$
		cbval2v.3	$⊢ Ⅎ x ψ$
		cbval2v.4	$⊢ Ⅎ y ψ$
		cbval2v.5	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
	Assertion	cbvex2v	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w ψ$

Proof

Step	Hyp	Ref	Expression
1		cbval2v.1	$⊢ Ⅎ z φ$
2		cbval2v.2	$⊢ Ⅎ w φ$
3		cbval2v.3	$⊢ Ⅎ x ψ$
4		cbval2v.4	$⊢ Ⅎ y ψ$
5		cbval2v.5	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
6	1	nfn	$⊢ Ⅎ z \neg φ$
7	2	nfn	$⊢ Ⅎ w \neg φ$
8	3	nfn	$⊢ Ⅎ x \neg ψ$
9	4	nfn	$⊢ Ⅎ y \neg ψ$
10	5	notbid	$⊢ (x = z \land y = w) \to (\neg φ \leftrightarrow \neg ψ)$
11	6 7 8 9 10	cbval2v	$⊢ \forall x \forall y \neg φ \leftrightarrow \forall z \forall w \neg ψ$
12		2nexaln	$⊢ \neg \exists x \exists y φ \leftrightarrow \forall x \forall y \neg φ$
13		2nexaln	$⊢ \neg \exists z \exists w ψ \leftrightarrow \forall z \forall w \neg ψ$
14	11 12 13	3bitr4i	$⊢ \neg \exists x \exists y φ \leftrightarrow \neg \exists z \exists w ψ$
15	14	con4bii	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w ψ$