Theorem membpartlem19

Description: Together with disjlem19 , this is former prtlem19 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 21-Oct-2021)

	Ref	Expression
Assertion	membpartlem19	⊢ ( 𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ( ( 𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfmembpart2	⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )
2		n0el2	⊢ ( ¬ ∅ ∈ 𝐴 ↔ dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
3	2	biimpi	⊢ ( ¬ ∅ ∈ 𝐴 → dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
4	3	ad2antll	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
5	4	eleq2d	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ↔ 𝑢 ∈ 𝐴 ) )
6		eldisjlem19	⊢ ( 𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
7	6	adantrd	⊢ ( 𝐵 ∈ 𝑉 → ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
8	7	imp	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) )
9	8	expd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
10	5 9	sylbird	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝐴 → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
11	1 10	sylan2b	⊢ ( ( 𝐵 ∈ 𝑉 ∧ MembPart 𝐴 ) → ( 𝑢 ∈ 𝐴 → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
12	11	impd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ MembPart 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) )
13	12	ex	⊢ ( 𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ( ( 𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )