Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997) (Proof shortened by Steven Nguyen, 5-May-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | raleqbi1dv.1 | |
|
Assertion | rexeqbi1dv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbi1dv.1 | |
|
2 | id | |
|
3 | 2 1 | rexeqbidvv | |