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

Metamath Proof Explorer

Theorem rexrnmptw

Description: A restricted quantifier over an image set. Version of rexrnmpt with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Aug-2015) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

		Ref	Expression
	Hypotheses	rexrnmptw.1	$⊢ F = (x \in A ⟼ B)$
		rexrnmptw.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
	Assertion	rexrnmptw	$⊢ \forall x \in A B \in V \to (\exists y \in ran F ψ \leftrightarrow \exists x \in A χ)$

Proof

Step	Hyp	Ref	Expression
1		rexrnmptw.1	$⊢ F = (x \in A ⟼ B)$
2		rexrnmptw.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3	2	notbid	$⊢ y = B \to (\neg ψ \leftrightarrow \neg χ)$
4	1 3	ralrnmptw	$⊢ \forall x \in A B \in V \to (\forall y \in ran F \neg ψ \leftrightarrow \forall x \in A \neg χ)$
5	4	notbid	$⊢ \forall x \in A B \in V \to (\neg \forall y \in ran F \neg ψ \leftrightarrow \neg \forall x \in A \neg χ)$
6		dfrex2	$⊢ \exists y \in ran F ψ \leftrightarrow \neg \forall y \in ran F \neg ψ$
7		dfrex2	$⊢ \exists x \in A χ \leftrightarrow \neg \forall x \in A \neg χ$
8	5 6 7	3bitr4g	$⊢ \forall x \in A B \in V \to (\exists y \in ran F ψ \leftrightarrow \exists x \in A χ)$