Theorem ralabsobidv

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

	Ref	Expression
Hypotheses	ralabsod.1	|- ( ph -> Tr M )
	ralabsobidv.2	|- ( ph -> ( ps <-> ch ) )
Assertion	ralabsobidv	|- ( ( ph /\ A e. M ) -> ( A. x e. A ps <-> A. x e. M ( x e. A -> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralabsod.1	|- ( ph -> Tr M )
2		ralabsobidv.2	|- ( ph -> ( ps <-> ch ) )
3	2	ralbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
4	3	adantr	|- ( ( ph /\ A e. M ) -> ( A. x e. A ps <-> A. x e. A ch ) )
5	1	ralabsod	|- ( ( ph /\ A e. M ) -> ( A. x e. A ch <-> A. x e. M ( x e. A -> ch ) ) )
6	4 5	bitrd	|- ( ( ph /\ A e. M ) -> ( A. x e. A ps <-> A. x e. M ( x e. A -> ch ) ) )