Metamath Proof Explorer


Theorem cbvmowOLD

Description: Obsolete version of cbvmow as of 23-May-2024. (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cbvmowOLD.1 𝑦 𝜑
cbvmowOLD.2 𝑥 𝜓
cbvmowOLD.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvmowOLD ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvmowOLD.1 𝑦 𝜑
2 cbvmowOLD.2 𝑥 𝜓
3 cbvmowOLD.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
4 1 sb8ev ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
5 1 sb8euv ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
6 4 5 imbi12i ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
7 moeu ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
8 moeu ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
9 6 7 8 3bitr4i ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
10 2 3 sbiev ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
11 10 mobii ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃* 𝑦 𝜓 )
12 9 11 bitri ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )