Metamath Proof Explorer

Theorem issetssr

Description: Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019)

Ref Expression
Assertion issetssr 
|- ( A e. _V <-> A _S A )

Proof

Step Hyp Ref Expression
1 brssrid 
 |-  ( A e. _V -> A _S A )
2 relssr 
 |-  Rel _S
3 2 brrelex1i 
 |-  ( A _S A -> A e. _V )
4 1 3 impbii 
 |-  ( A e. _V <-> A _S A )