disjlem19

		Ref	Expression
	Assertion	disjlem19	$⊢ A \in V \to (Disj R \to ((x \in dom R \land A \in [x] R) \to [x] R = [A] ≀ R))$

Step	Hyp	Ref	Expression
1		disjlem18	$⊢ (A \in V \land z \in V) \to (Disj R \to ((x \in dom R \land A \in [x] R) \to (z \in [x] R \leftrightarrow A ≀ R z)))$
2	1	elvd	$⊢ A \in V \to (Disj R \to ((x \in dom R \land A \in [x] R) \to (z \in [x] R \leftrightarrow A ≀ R z)))$
3	2	imp31	$⊢ ((A \in V \land Disj R) \land (x \in dom R \land A \in [x] R)) \to (z \in [x] R \leftrightarrow A ≀ R z)$
4		elecALTV	$⊢ (A \in V \land z \in V) \to (z \in [A] ≀ R \leftrightarrow A ≀ R z)$
5	4	elvd	$⊢ A \in V \to (z \in [A] ≀ R \leftrightarrow A ≀ R z)$
6	5	ad2antrr	$⊢ ((A \in V \land Disj R) \land (x \in dom R \land A \in [x] R)) \to (z \in [A] ≀ R \leftrightarrow A ≀ R z)$
7	3 6	bitr4d	$⊢ ((A \in V \land Disj R) \land (x \in dom R \land A \in [x] R)) \to (z \in [x] R \leftrightarrow z \in [A] ≀ R)$
8	7	eqrdv	$⊢ ((A \in V \land Disj R) \land (x \in dom R \land A \in [x] R)) \to [x] R = [A] ≀ R$
9	8	exp31	$⊢ A \in V \to (Disj R \to ((x \in dom R \land A \in [x] R) \to [x] R = [A] ≀ R))$

Metamath Proof Explorer