Theorem eldmres3

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	eldmres3	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldmres2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) ) )
2		n0	⊢ ( [ 𝐵 ] 𝑅 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 )
3	2	anbi2i	⊢ ( ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) )
4	1 3	bitr4di	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )