Theorem eldmres2

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020)

	Ref	Expression
Assertion	eldmres2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldmres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )
2		eldmg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom 𝑅 ↔ ∃ 𝑦 𝐵 𝑅 𝑦 ) )
3		eldm4	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) )
4	2 3	bitr3d	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑦 𝐵 𝑅 𝑦 ↔ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) )
5	4	anbi2d	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) ) )
6	1 5	bitrd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ [ 𝐵 ] 𝑅 ) ) )