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 ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elisset ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
2 biimt ⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( 𝐴 ∈ 𝐵 ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ) )
4 19.23v ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
5 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
6 5 bicomd ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
7 6 pm5.74i ⊢ ( ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
8 7 albii ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
9 4 8 bitr3i ⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
10 3 9 bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ) )