Metamath Proof Explorer


Theorem cbvreuw

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 10-Dec-2024)

Ref Expression
Hypotheses cbvreuw.1 y φ
cbvreuw.2 x ψ
cbvreuw.3 x = y φ ψ
Assertion cbvreuw ∃! x A φ ∃! y A ψ

Proof

Step Hyp Ref Expression
1 cbvreuw.1 y φ
2 cbvreuw.2 x ψ
3 cbvreuw.3 x = y φ ψ
4 1 2 3 cbvrexw x A φ y A ψ
5 1 2 3 cbvrmow * x A φ * y A ψ
6 4 5 anbi12i x A φ * x A φ y A ψ * y A ψ
7 reu5 ∃! x A φ x A φ * x A φ
8 reu5 ∃! y A ψ y A ψ * y A ψ
9 6 7 8 3bitr4i ∃! x A φ ∃! y A ψ