Theorem bj-inrab2

Description: Shorter proof of inrab . (Contributed by BJ, 21-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-inrab2	$$⊢\left\{x\in A|\phi \right\}\cap \left\{x\in A|\psi \right\}=\left\{x\in A|\left(\phi \wedge \psi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-inrab	$$⊢\left\{x\in A|\phi \right\}\cap \left\{x\in A|\psi \right\}=\left\{x\in \left(A\cap A\right)|\left(\phi \wedge \psi \right)\right\}$$
2		nfv	$$⊢Ⅎx\top$$
3		inidm	$$⊢A\cap A=A$$
4	3	a1i	$$⊢\top \to A\cap A=A$$
5	2 4	bj-rabeqd	$$⊢\top \to \left\{x\in \left(A\cap A\right)|\left(\phi \wedge \psi \right)\right\}=\left\{x\in A|\left(\phi \wedge \psi \right)\right\}$$
6	5	mptru	$$⊢\left\{x\in \left(A\cap A\right)|\left(\phi \wedge \psi \right)\right\}=\left\{x\in A|\left(\phi \wedge \psi \right)\right\}$$
7	1 6	eqtri	$$⊢\left\{x\in A|\phi \right\}\cap \left\{x\in A|\psi \right\}=\left\{x\in A|\left(\phi \wedge \psi \right)\right\}$$