This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clel2g

Description: Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993) Strengthen from sethood hypothesis to sethood antecedent. (Revised by BJ, 12-Feb-2022) Avoid ax-12 . (Revised by BJ, 1-Sep-2024)

Ref Expression
Assertion clel2g ⊢ A ∈ V → A ∈ B ↔ ∀ x x = A → x ∈ B

Proof

Step Hyp Ref Expression
1 elisset ⊢ A ∈ V → ∃ x x = A
2 biimt ⊢ ∃ x x = A → A ∈ B ↔ ∃ x x = A → A ∈ B
3 1 2 syl ⊢ A ∈ V → A ∈ B ↔ ∃ x x = A → A ∈ B
4 19.23v ⊢ ∀ x x = A → A ∈ B ↔ ∃ x x = A → A ∈ B
5 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
6 5 bicomd ⊢ x = A → A ∈ B ↔ x ∈ B
7 6 pm5.74i ⊢ x = A → A ∈ B ↔ x = A → x ∈ B
8 7 albii ⊢ ∀ x x = A → A ∈ B ↔ ∀ x x = A → x ∈ B
9 4 8 bitr3i ⊢ ∃ x x = A → A ∈ B ↔ ∀ x x = A → x ∈ B
10 3 9 bitrdi ⊢ A ∈ V → A ∈ B ↔ ∀ x x = A → x ∈ B