bj-inrab2

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

		Ref	Expression
	Assertion	bj-inrab2	$⊢ \{x \in A \| φ\} \cap \{x \in A \| ψ\} = \{x \in A \| (φ \land ψ)\}$

Step	Hyp	Ref	Expression
1		bj-inrab	$⊢ \{x \in A \| φ\} \cap \{x \in A \| ψ\} = \{x \in (A \cap A) \| (φ \land ψ)\}$
2		nfv	$⊢ Ⅎ x ⊤$
3		inidm	$⊢ A \cap A = A$
4	3	a1i	$⊢ ⊤ \to A \cap A = A$
5	2 4	rabeqd	$⊢ ⊤ \to \{x \in (A \cap A) \| (φ \land ψ)\} = \{x \in A \| (φ \land ψ)\}$
6	5	mptru	$⊢ \{x \in (A \cap A) \| (φ \land ψ)\} = \{x \in A \| (φ \land ψ)\}$
7	1 6	eqtri	$⊢ \{x \in A \| φ\} \cap \{x \in A \| ψ\} = \{x \in A \| (φ \land ψ)\}$

Metamath Proof Explorer