Theorem cbvmpt

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011) Add disjoint variable condition to avoid ax-13 . See cbvmptg for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024)

	Ref	Expression
Hypotheses	cbvmpt.1	$$⊢\underset{\_}{Ⅎ}yB$$
	cbvmpt.2	$$⊢\underset{\_}{Ⅎ}xC$$
	cbvmpt.3	$$⊢x=y\to B=C$$
Assertion	cbvmpt	$$⊢\left(x\in A⟼B\right)=\left(y\in A⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvmpt.1	$$⊢\underset{\_}{Ⅎ}yB$$
2		cbvmpt.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		cbvmpt.3	$$⊢x=y\to B=C$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
6	4 5 1 2 3	cbvmptf	$$⊢\left(x\in A⟼B\right)=\left(y\in A⟼C\right)$$