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	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \varnothing \in \left(A{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		zfreg	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \exists x\in Ax\cap A=\varnothing$$
2		eqcom	$$⊢x\cap A=\varnothing \leftrightarrow \varnothing =x\cap A$$
3	2	rexbii	$$⊢\exists x\in Ax\cap A=\varnothing \leftrightarrow \exists x\in A\varnothing =x\cap A$$
4	1 3	sylib	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \exists x\in A\varnothing =x\cap A$$
5		simpl	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to A\in V$$
6		elrest	$$⊢\left(A\in V\wedge A\in V\right)\to \left(\varnothing \in \left(A{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in A\varnothing =x\cap A\right)$$
7	5 6	syldan	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \left(\varnothing \in \left(A{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in A\varnothing =x\cap A\right)$$
8	4 7	mpbird	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \varnothing \in \left(A{\upharpoonright }_{𝑡}A\right)$$