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 𝑦 𝜑
cbveu.2 𝑥 𝜓
cbveu.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbveuALT ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 cbveu.1 𝑦 𝜑
2 cbveu.2 𝑥 𝜓
3 cbveu.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
4 1 2 3 cbvex ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 )
5 1 2 3 cbvmo ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )
6 4 5 anbi12i ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑦 𝜓 ∧ ∃* 𝑦 𝜓 ) )
7 df-eu ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
8 df-eu ( ∃! 𝑦 𝜓 ↔ ( ∃ 𝑦 𝜓 ∧ ∃* 𝑦 𝜓 ) )
9 6 7 8 3bitr4i ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )