Theorem rexabsobidv

Description: Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypotheses	ralabsod.1	⊢ ( 𝜑 → Tr 𝑀 )
	ralabsobidv.2	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	rexabsobidv	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralabsod.1	⊢ ( 𝜑 → Tr 𝑀 )
2		ralabsobidv.2	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
3	2	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 𝜒 ) )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 𝜒 ) )
5	1	rexabsod	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ 𝐴 𝜒 ↔ ∃ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
6	4 5	bitrd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )