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

Metamath Proof Explorer

Theorem clel4g

Description: Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993) Strengthen from sethood hypothesis to sethood antecedent and avoid ax-12 . (Revised by BJ, 1-Sep-2024)

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

Proof

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