cbvex2

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvex2v if possible. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 16-Jun-2019) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbval2.1	$⊢ Ⅎ z φ$
2		cbval2.2	$⊢ Ⅎ w φ$
3		cbval2.3	$⊢ Ⅎ x ψ$
4		cbval2.4	$⊢ Ⅎ y ψ$
5		cbval2.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	cbval2	$⊢ \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 ψ$

Metamath Proof Explorer

Theorem cbvex2

Proof