cbvrexfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf with a disjoint variable condition, which does not require ax-13 . For a version not dependent on ax-11 and ax-12, see cbvrexvw . (Contributed by FL, 27-Apr-2008) Avoid ax-10 , ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvrexfw.1	$⊢ \underline{Ⅎ} x A$
	cbvrexfw.2	$⊢ \underline{Ⅎ} y A$
	cbvrexfw.3	$⊢ Ⅎ y φ$
	cbvrexfw.4	$⊢ Ⅎ x ψ$
	cbvrexfw.5	$⊢ x = y \to (φ \leftrightarrow ψ)$
Assertion	cbvrexfw	$⊢ \exists x \in A φ \leftrightarrow \exists y \in A ψ$

Proof

Step	Hyp	Ref	Expression
1		cbvrexfw.1	$⊢ \underline{Ⅎ} x A$
2		cbvrexfw.2	$⊢ \underline{Ⅎ} y A$
3		cbvrexfw.3	$⊢ Ⅎ y φ$
4		cbvrexfw.4	$⊢ Ⅎ x ψ$
5		cbvrexfw.5	$⊢ x = y \to (φ \leftrightarrow ψ)$
6	3	nfn	$⊢ Ⅎ y \neg φ$
7	4	nfn	$⊢ Ⅎ x \neg ψ$
8	5	notbid	$⊢ x = y \to (\neg φ \leftrightarrow \neg ψ)$
9	1 2 6 7 8	cbvralfw	$⊢ \forall x \in A \neg φ \leftrightarrow \forall y \in A \neg ψ$
10		ralnex	$⊢ \forall x \in A \neg φ \leftrightarrow \neg \exists x \in A φ$
11		ralnex	$⊢ \forall y \in A \neg ψ \leftrightarrow \neg \exists y \in A ψ$
12	9 10 11	3bitr3i	$⊢ \neg \exists x \in A φ \leftrightarrow \neg \exists y \in A ψ$
13	12	con4bii	$⊢ \exists x \in A φ \leftrightarrow \exists y \in A ψ$

Metamath Proof Explorer

Theorem cbvrexfw

Proof