Theorem eldmqsres2

Description: Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020)

	Ref	Expression
Assertion	eldmqsres2	|- ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A E. x e. [ u ] R B = [ u ] R ) )

Proof

Step	Hyp	Ref	Expression
1		eldmqsres	|- ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A ( E. x x e. [ u ] R /\ B = [ u ] R ) ) )
2		df-rex	|- ( E. x e. [ u ] R B = [ u ] R <-> E. x ( x e. [ u ] R /\ B = [ u ] R ) )
3		19.41v	|- ( E. x ( x e. [ u ] R /\ B = [ u ] R ) <-> ( E. x x e. [ u ] R /\ B = [ u ] R ) )
4	2 3	bitri	|- ( E. x e. [ u ] R B = [ u ] R <-> ( E. x x e. [ u ] R /\ B = [ u ] R ) )
5	4	rexbii	|- ( E. u e. A E. x e. [ u ] R B = [ u ] R <-> E. u e. A ( E. x x e. [ u ] R /\ B = [ u ] R ) )
6	1 5	bitr4di	|- ( B e. V -> ( B e. ( dom ( R |` A ) /. ( R |` A ) ) <-> E. u e. A E. x e. [ u ] R B = [ u ] R ) )