Theorem ecelqsi

Description: Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypothesis	ecelqsi.1	⊢ 𝑅 ∈ V
Assertion	ecelqsi	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ecelqsi.1	⊢ 𝑅 ∈ V
2		ecelqsg	⊢ ( ( 𝑅 ∈ V ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
3	1 2	mpan	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )