This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-cbvex2vv

Description: Version of cbvex2vv with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	bj-cbval2vv.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
	Assertion	bj-cbvex2vv	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w ψ$

Proof

Step	Hyp	Ref	Expression
1		bj-cbval2vv.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
2		nfv	$⊢ Ⅎ z φ$
3		nfv	$⊢ Ⅎ w φ$
4		nfv	$⊢ Ⅎ x ψ$
5		nfv	$⊢ Ⅎ y ψ$
6	2 3 4 5 1	cbvex2v	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w ψ$