Metamath Proof Explorer

Theorem bj-elid3

Description: Characterization of the couples in _I whose first component is a setvar. (Contributed by BJ, 29-Mar-2020)

Ref Expression
Assertion bj-elid3 
|- ( <. x , A >. e. _I <-> x = A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 bj-opelidb1 
 |-  ( <. x , A >. e. _I <-> ( x e. _V /\ x = A ) )
3 1 2 mpbiran 
 |-  ( <. x , A >. e. _I <-> x = A )