Theorem bj-rcleq

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

	Ref	Expression
Assertion	bj-rcleq	⊢ ( ( 𝑉 ∩ 𝐴 ) = ( 𝑉 ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑥 𝐴
2		nfcv	⊢ Ⅎ 𝑥 𝐵
3		nfcv	⊢ Ⅎ 𝑥 𝑉
4	1 2 3	bj-rcleqf	⊢ ( ( 𝑉 ∩ 𝐴 ) = ( 𝑉 ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )