cbvrexsvwOLD

Description: Obsolete version of cbvrexsvw as of 8-Mar-2025. (Contributed by NM, 20-Nov-2005) Avoid ax-13 . (Revised by GG, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	cbvrexsvwOLD	$⊢ \exists x \in A φ \leftrightarrow \exists y \in A [y/ x] φ$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ z φ$
2		nfs1v	$⊢ Ⅎ x [z/ x] φ$
3		sbequ12	$⊢ x = z \to (φ \leftrightarrow [z/ x] φ)$
4	1 2 3	cbvrexw	$⊢ \exists x \in A φ \leftrightarrow \exists z \in A [z/ x] φ$
5		nfv	$⊢ Ⅎ y [z/ x] φ$
6		nfv	$⊢ Ⅎ z [y/ x] φ$
7		sbequ	$⊢ z = y \to ([z/ x] φ \leftrightarrow [y/ x] φ)$
8	5 6 7	cbvrexw	$⊢ \exists z \in A [z/ x] φ \leftrightarrow \exists y \in A [y/ x] φ$
9	4 8	bitri	$⊢ \exists x \in A φ \leftrightarrow \exists y \in A [y/ x] φ$

Metamath Proof Explorer

Theorem cbvrexsvwOLD

Proof