Metamath Proof Explorer

Theorem cbvrabv

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 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion cbvrabv ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{y}\in {A}|{\psi }\right\}$

Proof

Step Hyp Ref Expression
1 cbvrabv.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
3 2 1 anbi12d ${⊢}{x}={y}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({y}\in {A}\wedge {\psi }\right)\right)$
4 3 cbvabv ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}=\left\{{y}|\left({y}\in {A}\wedge {\psi }\right)\right\}$
5 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
6 df-rab ${⊢}\left\{{y}\in {A}|{\psi }\right\}=\left\{{y}|\left({y}\in {A}\wedge {\psi }\right)\right\}$
7 4 5 6 3eqtr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{y}\in {A}|{\psi }\right\}$