Metamath Proof Explorer

Theorem bj-rcleqf

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

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

Proof

Step Hyp Ref Expression
1 bj-rcleqf.a ⊢ Ⅎ _ x A
2 bj-rcleqf.b ⊢ Ⅎ _ x B
3 bj-rcleqf.v ⊢ Ⅎ _ x V
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 ⊢ ∀ x x ∈ V ∩ A ↔ x ∈ V ∩ B ↔ ∀ x x ∈ V → x ∈ A ↔ x ∈ B
10 3 1 nfin ⊢ Ⅎ _ x V ∩ A
11 3 2 nfin ⊢ Ⅎ _ x V ∩ B
12 10 11 cleqf ⊢ V ∩ A = V ∩ B ↔ ∀ x x ∈ V ∩ A ↔ x ∈ V ∩ B
13 df-ral ⊢ ∀ x ∈ V x ∈ A ↔ x ∈ B ↔ ∀ x x ∈ V → x ∈ A ↔ x ∈ B
14 9 12 13 3bitr4i ⊢ V ∩ A = V ∩ B ↔ ∀ x ∈ V x ∈ A ↔ x ∈ B