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 I x = A


Step Hyp Ref Expression
1 vex x V
2 bj-opelidb1 x A I x V x = A
3 1 2 mpbiran x A I x = A