Metamath Proof Explorer

Theorem dmqseqim2

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

		Ref	Expression
	Assertion	dmqseqim2	\|- ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ( B e. ran R <-> B e. U. A ) ) ) )

Step	Hyp	Ref	Expression
1		dmqseqim	\|- ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ran R = U. A ) ) )
2		eleq2	\|- ( ran R = U. A -> ( B e. ran R <-> B e. U. A ) )
3	1 2	syl8	\|- ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ( B e. ran R <-> B e. U. A ) ) ) )

Step

Hyp

Ref

Expression

 |-  ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ran R = U. A ) ) )

 |-  ( ran R = U. A -> ( B e. ran R <-> B e. U. A ) )

1 2

 |-  ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ( B e. ran R <-> B e. U. A ) ) ) )