Theorem 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	rabeqd.nf	|- F/ x ph
	rabeqd.1	|- ( ph -> A = B )
Assertion	rabeqd	|- ( ph -> { x e. A | ps } = { x e. B | ps } )

Proof

Step	Hyp	Ref	Expression
1		rabeqd.nf	|- F/ x ph
2		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	rabbida4	|- ( ph -> { x e. A | ps } = { x e. B | ps } )