Theorem ralabsod

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

	Ref	Expression
Hypothesis	ralabsod.1	⊢ ( 𝜑 → Tr 𝑀 )
Assertion	ralabsod	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑀 ) → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralabsod.1	⊢ ( 𝜑 → Tr 𝑀 )
2		ralabso	⊢ ( ( Tr 𝑀 ∧ 𝐴 ∈ 𝑀 ) → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) )
3	1 2	sylan	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑀 ) → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) )