Metamath Proof Explorer

Theorem bj-inex1gALT

Description: Proof of inex1g from sepg to then allow proving inex1 from it. That does not reduce the combined proof size of inex1 and inex1g . (Contributed by BJ, 14-Jul-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-inex1gALT ⊢ A ∈ V → A ∩ B ∈ V

Proof

Step Hyp Ref Expression
1 sepg ⊢ A ∈ V → ∃ x ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
2 dfcleq ⊢ x = A ∩ B ↔ ∀ y y ∈ x ↔ y ∈ A ∩ B
3 elin ⊢ y ∈ A ∩ B ↔ y ∈ A ∧ y ∈ B
4 3 a1i ⊢ A ∈ V → y ∈ A ∩ B ↔ y ∈ A ∧ y ∈ B
5 4 bibi2d ⊢ A ∈ V → y ∈ x ↔ y ∈ A ∩ B ↔ y ∈ x ↔ y ∈ A ∧ y ∈ B
6 5 albidv ⊢ A ∈ V → ∀ y y ∈ x ↔ y ∈ A ∩ B ↔ ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
7 2 6 bitrid ⊢ A ∈ V → x = A ∩ B ↔ ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
8 7 exbidv ⊢ A ∈ V → ∃ x x = A ∩ B ↔ ∃ x ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
9 1 8 mpbird ⊢ A ∈ V → ∃ x x = A ∩ B
10 isset ⊢ A ∩ B ∈ V ↔ ∃ x x = A ∩ B
11 9 10 sylibr ⊢ A ∈ V → A ∩ B ∈ V