Theorem bj-rabeqd

Description: Deduction form of rabeq . Note that contrary to rabeq it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019)

	Ref	Expression
Hypotheses	bj-rabeqd.nf	|- F/ x ph
	bj-rabeqd.1	|- ( ph -> A = B )
Assertion	bj-rabeqd	|- ( ph -> { x e. A | ps } = { x e. B | ps } )

Proof

Step	Hyp	Ref	Expression
1		bj-rabeqd.nf	|- F/ x ph
2		bj-rabeqd.1	|- ( ph -> A = B )
3		eleq2	|- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi1d	|- ( A = B -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ps ) ) )
5	2 4	syl	|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ps ) ) )
6	1 5	bj-rabbida2	|- ( ph -> { x e. A | ps } = { x e. B | ps } )