Theorem ralabsobidv

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

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

Proof

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