Theorem eldmres

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019)

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

Proof

Step	Hyp	Ref	Expression
1		eldmg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑦 𝐵 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
2		brres	⊢ ( 𝑦 ∈ V → ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) ) )
3	2	elv	⊢ ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) )
4	3	exbii	⊢ ( ∃ 𝑦 𝐵 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ∃ 𝑦 ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) )
5		19.42v	⊢ ( ∃ 𝑦 ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) )
6	4 5	bitri	⊢ ( ∃ 𝑦 𝐵 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) )
7	1 6	bitrdi	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )