Theorem dmqseqim2

Description: Lemma for erimeq2 . (Contributed by Peter Mazsa, 29-Dec-2021)

	Ref	Expression
Assertion	dmqseqim2	$$⊢R\in V\to \left(\mathrm{Rel}R\to \left(\mathrm{dom}R/R=A\to \left(B\in \mathrm{ran}R\leftrightarrow B\in \bigcup A\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmqseqim	$$⊢R\in V\to \left(\mathrm{Rel}R\to \left(\mathrm{dom}R/R=A\to \mathrm{ran}R=\bigcup A\right)\right)$$
2		eleq2	$$⊢\mathrm{ran}R=\bigcup A\to \left(B\in \mathrm{ran}R\leftrightarrow B\in \bigcup A\right)$$
3	1 2	syl8	$$⊢R\in V\to \left(\mathrm{Rel}R\to \left(\mathrm{dom}R/R=A\to \left(B\in \mathrm{ran}R\leftrightarrow B\in \bigcup A\right)\right)\right)$$