Theorem raleqbidvv

Description: Version of raleqbidv with additional disjoint variable conditions, not requiring ax-8 nor df-clel . (Contributed by BJ, 22-Sep-2024)

	Ref	Expression
Hypotheses	raleqbidvv.1	|- ( ph -> A = B )
	raleqbidvv.2	|- ( ph -> ( ps <-> ch ) )
Assertion	raleqbidvv	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Proof

Step	Hyp	Ref	Expression
1		raleqbidvv.1	|- ( ph -> A = B )
2		raleqbidvv.2	|- ( ph -> ( ps <-> ch ) )
3	2	alrimiv	|- ( ph -> A. x ( ps <-> ch ) )
4		dfcleq	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )
5	1 4	sylib	|- ( ph -> A. x ( x e. A <-> x e. B ) )
6		19.26	|- ( A. x ( ( ps <-> ch ) /\ ( x e. A <-> x e. B ) ) <-> ( A. x ( ps <-> ch ) /\ A. x ( x e. A <-> x e. B ) ) )
7	3 5 6	sylanbrc	|- ( ph -> A. x ( ( ps <-> ch ) /\ ( x e. A <-> x e. B ) ) )
8		imbi12	|- ( ( x e. A <-> x e. B ) -> ( ( ps <-> ch ) -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) ) )
9	8	impcom	|- ( ( ( ps <-> ch ) /\ ( x e. A <-> x e. B ) ) -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )
10	7 9	sylg	|- ( ph -> A. x ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )
11		albi	|- ( A. x ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
12	10 11	syl	|- ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
13		df-ral	|- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
14		df-ral	|- ( A. x e. B ch <-> A. x ( x e. B -> ch ) )
15	12 13 14	3bitr4g	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )