Metamath Proof Explorer


Theorem cbveuALT

Description: Alternative proof of cbveu . Since df-eu combines two other quantifiers, one can base this theorem on their associated 'change bounded variable' kind of theorems as well. (Contributed by Wolf Lammen, 5-Jan-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cbveu.1 yφ
cbveu.2 xψ
cbveu.3 x=yφψ
Assertion cbveuALT ∃!xφ∃!yψ

Proof

Step Hyp Ref Expression
1 cbveu.1 yφ
2 cbveu.2 xψ
3 cbveu.3 x=yφψ
4 1 2 3 cbvex xφyψ
5 1 2 3 cbvmo *xφ*yψ
6 4 5 anbi12i xφ*xφyψ*yψ
7 df-eu ∃!xφxφ*xφ
8 df-eu ∃!yψyψ*yψ
9 6 7 8 3bitr4i ∃!xφ∃!yψ