Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999) Require x , y be disjoint to avoid ax-11 and ax-13 . (Revised by Steven Nguyen, 4-Dec-2022)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvrabv.1 | ||
Assertion | cbvrabv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrabv.1 | ||
2 | eleq1w | ||
3 | 2 1 | anbi12d | |
4 | 3 | cbvabv | |
5 | df-rab | ||
6 | df-rab | ||
7 | 4 5 6 | 3eqtr4i |