Metamath Proof Explorer

Theorem elinisegg

Description: Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Put in closed form and shorten proof. (Revised by BJ, 16-Oct-2024)

Ref Expression
Assertion elinisegg ⊢ B ∈ V ∧ C ∈ W → C ∈ A -1 B ↔ C A B

Proof

Step Hyp Ref Expression
1 elimasng1 ⊢ B ∈ V ∧ C ∈ W → C ∈ A -1 B ↔ B A -1 C
2 brcnvg ⊢ B ∈ V ∧ C ∈ W → B A -1 C ↔ C A B
3 1 2 bitrd ⊢ B ∈ V ∧ C ∈ W → C ∈ A -1 B ↔ C A B