cbvexv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex with a disjoint variable condition, which does not require ax-13 . See cbvexvw for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv for another variant. (Contributed by NM, 21-Jun-1993) (Revised by BJ, 31-May-2019)

	Ref	Expression
Hypotheses	cbvalv1.nf1	$⊢ Ⅎ y φ$
	cbvalv1.nf2	$⊢ Ⅎ x ψ$
	cbvalv1.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
Assertion	cbvexv1	$⊢ \exists x φ \leftrightarrow \exists y ψ$

Proof

Step	Hyp	Ref	Expression
1		cbvalv1.nf1	$⊢ Ⅎ y φ$
2		cbvalv1.nf2	$⊢ Ⅎ x ψ$
3		cbvalv1.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
4	1	nfn	$⊢ Ⅎ y \neg φ$
5	2	nfn	$⊢ Ⅎ x \neg ψ$
6	3	notbid	$⊢ x = y \to (\neg φ \leftrightarrow \neg ψ)$
7	4 5 6	cbvalv1	$⊢ \forall x \neg φ \leftrightarrow \forall y \neg ψ$
8		alnex	$⊢ \forall x \neg φ \leftrightarrow \neg \exists x φ$
9		alnex	$⊢ \forall y \neg ψ \leftrightarrow \neg \exists y ψ$
10	7 8 9	3bitr3i	$⊢ \neg \exists x φ \leftrightarrow \neg \exists y ψ$
11	10	con4bii	$⊢ \exists x φ \leftrightarrow \exists y ψ$

Metamath Proof Explorer

Theorem cbvexv1

Proof