Theorem ineqri

Description: Inference from membership to intersection. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	ineqri.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
Assertion	ineqri	⊢ ( 𝐴 ∩ 𝐵 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		ineqri.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
2		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
3	2 1	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
4	3	eqriv	⊢ ( 𝐴 ∩ 𝐵 ) = 𝐶