Theorem rexxfr3dALT

Description: Longer proof of rexxfr3d using ax-11 instead of ax-12 , without the disjoint variable condition A x y . (Contributed by SN, 19-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rexxfr3dALT.s	|- ( x = X -> ( ps <-> ch ) )
	rexxfr3dALT.x	|- ( ph -> ( x e. A <-> E. y e. B x = X ) )
	rexxfr3dALT.a	|- ( ph -> X e. V )
Assertion	rexxfr3dALT	|- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) )

Proof

Step	Hyp	Ref	Expression
1		rexxfr3dALT.s	|- ( x = X -> ( ps <-> ch ) )
2		rexxfr3dALT.x	|- ( ph -> ( x e. A <-> E. y e. B x = X ) )
3		rexxfr3dALT.a	|- ( ph -> X e. V )
4	2	anbi1d	|- ( ph -> ( ( x e. A /\ ps ) <-> ( E. y e. B x = X /\ ps ) ) )
5	1	pm5.32i	|- ( ( x = X /\ ps ) <-> ( x = X /\ ch ) )
6	5	rexbii	|- ( E. y e. B ( x = X /\ ps ) <-> E. y e. B ( x = X /\ ch ) )
7		r19.41v	|- ( E. y e. B ( x = X /\ ps ) <-> ( E. y e. B x = X /\ ps ) )
8	6 7	bitr3i	|- ( E. y e. B ( x = X /\ ch ) <-> ( E. y e. B x = X /\ ps ) )
9	4 8	bitr4di	|- ( ph -> ( ( x e. A /\ ps ) <-> E. y e. B ( x = X /\ ch ) ) )
10	9	exbidv	|- ( ph -> ( E. x ( x e. A /\ ps ) <-> E. x E. y e. B ( x = X /\ ch ) ) )
11		df-rex	|- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
12		19.41v	|- ( E. x ( x = X /\ ch ) <-> ( E. x x = X /\ ch ) )
13	12	rexbii	|- ( E. y e. B E. x ( x = X /\ ch ) <-> E. y e. B ( E. x x = X /\ ch ) )
14		rexcom4	|- ( E. y e. B E. x ( x = X /\ ch ) <-> E. x E. y e. B ( x = X /\ ch ) )
15	13 14	bitr3i	|- ( E. y e. B ( E. x x = X /\ ch ) <-> E. x E. y e. B ( x = X /\ ch ) )
16	10 11 15	3bitr4g	|- ( ph -> ( E. x e. A ps <-> E. y e. B ( E. x x = X /\ ch ) ) )
17		elisset	|- ( X e. V -> E. x x = X )
18	3 17	syl	|- ( ph -> E. x x = X )
19	18	biantrurd	|- ( ph -> ( ch <-> ( E. x x = X /\ ch ) ) )
20	19	rexbidv	|- ( ph -> ( E. y e. B ch <-> E. y e. B ( E. x x = X /\ ch ) ) )
21	16 20	bitr4d	|- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) )