Theorem rexabsod

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

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

Proof

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