Metamath Proof Explorer

Theorem rexabsod

Description: Deduction form of rexabso . (Contributed by Eric Schmidt, 19-Oct-2025)

		Ref	Expression
	Hypothesis	ralabsod.1	$⊢ φ \to Tr M$
	Assertion	rexabsod	$⊢ (φ \land A \in M) \to (\exists x \in A ψ \leftrightarrow \exists x \in M (x \in A \land ψ))$

Step	Hyp	Ref	Expression
1		ralabsod.1	$⊢ φ \to Tr M$
2		rexabso	$⊢ (Tr M \land A \in M) \to (\exists x \in A ψ \leftrightarrow \exists x \in M (x \in A \land ψ))$
3	1 2	sylan	$⊢ (φ \land A \in M) \to (\exists x \in A ψ \leftrightarrow \exists x \in M (x \in A \land ψ))$