Theorem prtlem11

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Assertion	prtlem11	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐶 ∈ 𝐴 → ( 𝐵 = [ 𝐶 ] ∼ → 𝐵 ∈ ( 𝐴 / ∼ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eceq1	⊢ ( 𝑥 = 𝐶 → [ 𝑥 ] ∼ = [ 𝐶 ] ∼ )
2	1	rspceeqv	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐵 = [ 𝐶 ] ∼ ) → ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] ∼ )
3		elqsg	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐵 ∈ ( 𝐴 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] ∼ ) )
4	2 3	imbitrrid	⊢ ( 𝐵 ∈ 𝐷 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐵 = [ 𝐶 ] ∼ ) → 𝐵 ∈ ( 𝐴 / ∼ ) ) )
5	4	expd	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐶 ∈ 𝐴 → ( 𝐵 = [ 𝐶 ] ∼ → 𝐵 ∈ ( 𝐴 / ∼ ) ) ) )