Metamath Proof Explorer

Theorem bj-rcleqf

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

Ref Expression
Hypotheses bj-rcleqf.a ⊢Ⅎ_xA
bj-rcleqf.b ⊢Ⅎ_xB
bj-rcleqf.v ⊢Ⅎ_xV
Assertion bj-rcleqf ⊢V∩A=V∩B↔∀x∈Vx∈A↔x∈B

Proof

Step Hyp Ref Expression
1 bj-rcleqf.a ⊢Ⅎ_xA
2 bj-rcleqf.b ⊢Ⅎ_xB
3 bj-rcleqf.v ⊢Ⅎ_xV
4 elin ⊢x∈V∩A↔x∈V∧x∈A
5 elin ⊢x∈V∩B↔x∈V∧x∈B
6 4 5 bibi12i ⊢x∈V∩A↔x∈V∩B↔x∈V∧x∈A↔x∈V∧x∈B
7 pm5.32 ⊢x∈V→x∈A↔x∈B↔x∈V∧x∈A↔x∈V∧x∈B
8 6 7 bitr4i ⊢x∈V∩A↔x∈V∩B↔x∈V→x∈A↔x∈B
9 8 albii ⊢∀xx∈V∩A↔x∈V∩B↔∀xx∈V→x∈A↔x∈B
10 3 1 nfin ⊢Ⅎ_xV∩A
11 3 2 nfin ⊢Ⅎ_xV∩B
12 10 11 cleqf ⊢V∩A=V∩B↔∀xx∈V∩A↔x∈V∩B
13 df-ral ⊢∀x∈Vx∈A↔x∈B↔∀xx∈V→x∈A↔x∈B
14 9 12 13 3bitr4i ⊢V∩A=V∩B↔∀x∈Vx∈A↔x∈B