Theorem bj-inrab2

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

	Ref	Expression
Assertion	bj-inrab2	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		bj-inrab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) ∣ ( 𝜑 ∧ 𝜓 ) }
2		nfv	⊢ Ⅎ 𝑥 ⊤
3		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
4	3	a1i	⊢ ( ⊤ → ( 𝐴 ∩ 𝐴 ) = 𝐴 )
5	2 4	bj-rabeqd	⊢ ( ⊤ → { 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) ∣ ( 𝜑 ∧ 𝜓 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) } )
6	5	mptru	⊢ { 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) ∣ ( 𝜑 ∧ 𝜓 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) }
7	1 6	eqtri	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) }