Metamath Proof Explorer


Theorem cbveuwOLD

Description: Obsolete version of cbveuw as of 23-May-2024. (Contributed by NM, 25-Nov-1994) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbveuwOLD.1 yφ
2 cbveuwOLD.2 xψ
3 cbveuwOLD.3 x=yφψ
4 1 sb8euv ∃!xφ∃!yyxφ
5 2 3 sbiev yxφψ
6 5 eubii ∃!yyxφ∃!yψ
7 4 6 bitri ∃!xφ∃!yψ