This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ Ⅎ _ y B
cbvmpt.2 ⊢ Ⅎ _ x C
cbvmpt.3 ⊢ x = y → B = C
Assertion cbvmpt ⊢ x ∈ A ⟼ B = y ∈ A ⟼ C

Proof

Step Hyp Ref Expression
1 cbvmpt.1 ⊢ Ⅎ _ y B
2 cbvmpt.2 ⊢ Ⅎ _ x C
3 cbvmpt.3 ⊢ x = y → B = C
4 nfcv ⊢ Ⅎ _ x A
5 nfcv ⊢ Ⅎ _ y A
6 4 5 1 2 3 cbvmptf ⊢ x ∈ A ⟼ B = y ∈ A ⟼ C