Theorem eldmqsres2

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

	Ref	Expression
Assertion	eldmqsres2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) / ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eldmqsres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) / ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑢 ] 𝑅 ) ) )
2		df-rex	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ↔ ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑢 ] 𝑅 ) )
3		19.41v	⊢ ( ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑢 ] 𝑅 ) ↔ ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑢 ] 𝑅 ) )
4	2 3	bitri	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ↔ ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑢 ] 𝑅 ) )
5	4	rexbii	⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ↔ ∃ 𝑢 ∈ 𝐴 ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑢 ] 𝑅 ) )
6	1 5	bitr4di	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) / ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ) )