Metamath Proof Explorer

Theorem bj-clel3gALT

Description: Alternate proof of clel3g . (Contributed by BJ, 1-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-clel3gALT ⊢ B ∈ V → A ∈ B ↔ ∃ x x = B ∧ A ∈ x

Proof

Step Hyp Ref Expression
1 elisset ⊢ B ∈ V → ∃ x x = B
2 1 biantrurd ⊢ B ∈ V → A ∈ B ↔ ∃ x x = B ∧ A ∈ B
3 19.41v ⊢ ∃ x x = B ∧ A ∈ B ↔ ∃ x x = B ∧ A ∈ B
4 2 3 bitr4di ⊢ B ∈ V → A ∈ B ↔ ∃ x x = B ∧ A ∈ B
5 eleq2 ⊢ x = B → A ∈ x ↔ A ∈ B
6 5 bicomd ⊢ x = B → A ∈ B ↔ A ∈ x
7 6 pm5.32i ⊢ x = B ∧ A ∈ B ↔ x = B ∧ A ∈ x
8 7 exbii ⊢ ∃ x x = B ∧ A ∈ B ↔ ∃ x x = B ∧ A ∈ x
9 4 8 bitrdi ⊢ B ∈ V → A ∈ B ↔ ∃ x x = B ∧ A ∈ x