cbvex

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out cbvexvw , cbvexv1 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbval.1	$⊢ Ⅎ y φ$
	cbval.2	$⊢ Ⅎ x ψ$
	cbval.3	$⊢ x = y \to (φ \leftrightarrow ψ)$
Assertion	cbvex	$⊢ \exists x φ \leftrightarrow \exists y ψ$

Proof

Step	Hyp	Ref	Expression
1		cbval.1	$⊢ Ⅎ y φ$
2		cbval.2	$⊢ Ⅎ x ψ$
3		cbval.3	$⊢ 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	cbval	$⊢ \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 cbvex

Proof