Theorem bj-restreg

Description: A reformulation of the axiom of regularity using elementwise intersection. (RK: might have to be placed later since theorems in this section are to be moved early (in the section related to the algebra of sets).) (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restreg	|- ( ( A e. V /\ A =/= (/) ) -> (/) e. ( A |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		zfreg	|- ( ( A e. V /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )
2		eqcom	|- ( ( x i^i A ) = (/) <-> (/) = ( x i^i A ) )
3	2	rexbii	|- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A (/) = ( x i^i A ) )
4	1 3	sylib	|- ( ( A e. V /\ A =/= (/) ) -> E. x e. A (/) = ( x i^i A ) )
5		simpl	|- ( ( A e. V /\ A =/= (/) ) -> A e. V )
6		elrest	|- ( ( A e. V /\ A e. V ) -> ( (/) e. ( A |`t A ) <-> E. x e. A (/) = ( x i^i A ) ) )
7	5 6	syldan	|- ( ( A e. V /\ A =/= (/) ) -> ( (/) e. ( A |`t A ) <-> E. x e. A (/) = ( x i^i A ) ) )
8	4 7	mpbird	|- ( ( A e. V /\ A =/= (/) ) -> (/) e. ( A |`t A ) )