Metamath Proof Explorer

Theorem iseqsetvlem

Description: Lemma for iseqsetv-cleq . (Contributed by Wolf Lammen, 17-Aug-2025) (Proof modification is discouraged.)

Ref Expression
Assertion iseqsetvlem 
|- ( E. x x = A <-> E. z z = A )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = z -> ( x = A <-> z = A ) )
2 1 cbvexvw 
 |-  ( E. x x = A <-> E. z z = A )