membpartlem19

		Ref	Expression
	Assertion	membpartlem19	$⊢ B \in V \to (MembPart A \to ((u \in A \land B \in u) \to u = [B] \sim A))$

Step	Hyp	Ref	Expression
1		dfmembpart2	$⊢ MembPart A \leftrightarrow (ElDisj A \land \neg \emptyset \in A)$
2		n0el2	$⊢ \neg \emptyset \in A \leftrightarrow dom ({E^{-1} ↾}_{A}) = A$
3	2	biimpi	$⊢ \neg \emptyset \in A \to dom ({E^{-1} ↾}_{A}) = A$
4	3	ad2antll	$⊢ (B \in V \land (ElDisj A \land \neg \emptyset \in A)) \to dom ({E^{-1} ↾}_{A}) = A$
5	4	eleq2d	$⊢ (B \in V \land (ElDisj A \land \neg \emptyset \in A)) \to (u \in dom ({E^{-1} ↾}_{A}) \leftrightarrow u \in A)$
6		eldisjlem19	$⊢ B \in V \to (ElDisj A \to ((u \in dom ({E^{-1} ↾}_{A}) \land B \in u) \to u = [B] \sim A))$
7	6	adantrd	$⊢ B \in V \to ((ElDisj A \land \neg \emptyset \in A) \to ((u \in dom ({E^{-1} ↾}_{A}) \land B \in u) \to u = [B] \sim A))$
8	7	imp	$⊢ (B \in V \land (ElDisj A \land \neg \emptyset \in A)) \to ((u \in dom ({E^{-1} ↾}_{A}) \land B \in u) \to u = [B] \sim A)$
9	8	expd	$⊢ (B \in V \land (ElDisj A \land \neg \emptyset \in A)) \to (u \in dom ({E^{-1} ↾}_{A}) \to (B \in u \to u = [B] \sim A))$
10	5 9	sylbird	$⊢ (B \in V \land (ElDisj A \land \neg \emptyset \in A)) \to (u \in A \to (B \in u \to u = [B] \sim A))$
11	1 10	sylan2b	$⊢ (B \in V \land MembPart A) \to (u \in A \to (B \in u \to u = [B] \sim A))$
12	11	impd	$⊢ (B \in V \land MembPart A) \to ((u \in A \land B \in u) \to u = [B] \sim A)$
13	12	ex	$⊢ B \in V \to (MembPart A \to ((u \in A \land B \in u) \to u = [B] \sim A))$

Metamath Proof Explorer