Metamath Proof Explorer

Theorem ralabsod

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

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

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