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 y φ
cbvmowOLD.2 x ψ
cbvmowOLD.3 x = y φ ψ
Assertion cbvmowOLD * x φ * y ψ

Proof

Step Hyp Ref Expression
1 cbvmowOLD.1 y φ
2 cbvmowOLD.2 x ψ
3 cbvmowOLD.3 x = y φ ψ
4 1 sb8ev x φ y y x φ
5 1 sb8euv ∃! x φ ∃! y y x φ
6 4 5 imbi12i x φ ∃! x φ y y x φ ∃! y y x φ
7 moeu * x φ x φ ∃! x φ
8 moeu * y y x φ y y x φ ∃! y y x φ
9 6 7 8 3bitr4i * x φ * y y x φ
10 2 3 sbiev y x φ ψ
11 10 mobii * y y x φ * y ψ
12 9 11 bitri * x φ * y ψ