cbvrexcsf

Description: A more general version of cbvrexf that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (Proof shortened by Mario Carneiro, 7-Dec-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	$⊢ \underline{Ⅎ} y A$
2		cbvralcsf.2	$⊢ \underline{Ⅎ} x B$
3		cbvralcsf.3	$⊢ Ⅎ y φ$
4		cbvralcsf.4	$⊢ Ⅎ x ψ$
5		cbvralcsf.5	$⊢ x = y \to A = B$
6		cbvralcsf.6	$⊢ x = y \to (φ \leftrightarrow ψ)$
7	3	nfn	$⊢ Ⅎ y \neg φ$
8	4	nfn	$⊢ Ⅎ x \neg ψ$
9	6	notbid	$⊢ x = y \to (\neg φ \leftrightarrow \neg ψ)$
10	1 2 7 8 5 9	cbvralcsf	$⊢ \forall x \in A \neg φ \leftrightarrow \forall y \in B \neg ψ$
11	10	notbii	$⊢ \neg \forall x \in A \neg φ \leftrightarrow \neg \forall y \in B \neg ψ$
12		dfrex2	$⊢ \exists x \in A φ \leftrightarrow \neg \forall x \in A \neg φ$
13		dfrex2	$⊢ \exists y \in B ψ \leftrightarrow \neg \forall y \in B \neg ψ$
14	11 12 13	3bitr4i	$⊢ \exists x \in A φ \leftrightarrow \exists y \in B ψ$

Metamath Proof Explorer

Theorem cbvrexcsf

Proof