Theorem bj-rcleqf

Description: Relative version of cleqf . (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Hypotheses	bj-rcleqf.a	|- F/_ x A
	bj-rcleqf.b	|- F/_ x B
	bj-rcleqf.v	|- F/_ x V
Assertion	bj-rcleqf	|- ( ( V i^i A ) = ( V i^i B ) <-> A. x e. V ( x e. A <-> x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		bj-rcleqf.a	|- F/_ x A
2		bj-rcleqf.b	|- F/_ x B
3		bj-rcleqf.v	|- F/_ x V
4		elin	|- ( x e. ( V i^i A ) <-> ( x e. V /\ x e. A ) )
5		elin	|- ( x e. ( V i^i B ) <-> ( x e. V /\ x e. B ) )
6	4 5	bibi12i	|- ( ( x e. ( V i^i A ) <-> x e. ( V i^i B ) ) <-> ( ( x e. V /\ x e. A ) <-> ( x e. V /\ x e. B ) ) )
7		pm5.32	|- ( ( x e. V -> ( x e. A <-> x e. B ) ) <-> ( ( x e. V /\ x e. A ) <-> ( x e. V /\ x e. B ) ) )
8	6 7	bitr4i	|- ( ( x e. ( V i^i A ) <-> x e. ( V i^i B ) ) <-> ( x e. V -> ( x e. A <-> x e. B ) ) )
9	8	albii	|- ( A. x ( x e. ( V i^i A ) <-> x e. ( V i^i B ) ) <-> A. x ( x e. V -> ( x e. A <-> x e. B ) ) )
10	3 1	nfin	|- F/_ x ( V i^i A )
11	3 2	nfin	|- F/_ x ( V i^i B )
12	10 11	cleqf	|- ( ( V i^i A ) = ( V i^i B ) <-> A. x ( x e. ( V i^i A ) <-> x e. ( V i^i B ) ) )
13		df-ral	|- ( A. x e. V ( x e. A <-> x e. B ) <-> A. x ( x e. V -> ( x e. A <-> x e. B ) ) )
14	9 12 13	3bitr4i	|- ( ( V i^i A ) = ( V i^i B ) <-> A. x e. V ( x e. A <-> x e. B ) )