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

Metamath Proof Explorer

Theorem bj-cbvexdv

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

		Ref	Expression
	Hypotheses	bj-cbvaldv.1	\|- F/ y ph
		bj-cbvaldv.2	\|- ( ph -> F/ y ps )
		bj-cbvaldv.3	\|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
	Assertion	bj-cbvexdv	\|- ( ph -> ( E. x ps <-> E. y ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbvaldv.1	\|- F/ y ph
2		bj-cbvaldv.2	\|- ( ph -> F/ y ps )
3		bj-cbvaldv.3	\|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
4	2	nfnd	\|- ( ph -> F/ y -. ps )
5		notbi	\|- ( ( ps <-> ch ) <-> ( -. ps <-> -. ch ) )
6	3 5	imbitrdi	\|- ( ph -> ( x = y -> ( -. ps <-> -. ch ) ) )
7	1 4 6	bj-cbvaldv	\|- ( ph -> ( A. x -. ps <-> A. y -. ch ) )
8	7	notbid	\|- ( ph -> ( -. A. x -. ps <-> -. A. y -. ch ) )
9		df-ex	\|- ( E. x ps <-> -. A. x -. ps )
10		df-ex	\|- ( E. y ch <-> -. A. y -. ch )
11	8 9 10	3bitr4g	\|- ( ph -> ( E. x ps <-> E. y ch ) )