Theorem rexabsobidv

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	rexabsobidv	|- ( ( ph /\ A e. M ) -> ( E. x e. A ps <-> E. 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	rexbidv	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
4	3	adantr	|- ( ( ph /\ A e. M ) -> ( E. x e. A ps <-> E. x e. A ch ) )
5	1	rexabsod	|- ( ( ph /\ A e. M ) -> ( E. x e. A ch <-> E. x e. M ( x e. A /\ ch ) ) )
6	4 5	bitrd	|- ( ( ph /\ A e. M ) -> ( E. x e. A ps <-> E. x e. M ( x e. A /\ ch ) ) )