Theorem prtlem9

Description: Lemma for prter3 . (Contributed by Rodolfo Medina, 25-Sep-2010)

	Ref	Expression
Assertion	prtlem9	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		risset	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝑥 = 𝐴 )
2		eceq1	⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )
3	2	reximi	⊢ ( ∃ 𝑥 ∈ 𝐵 𝑥 = 𝐴 → ∃ 𝑥 ∈ 𝐵 [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )
4	1 3	sylbi	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )