Theorem eldm1cossres2

Description: Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018)

	Ref	Expression
Assertion	eldm1cossres2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ [ 𝑥 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eldm1cossres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ) )
2		elecALTV	⊢ ( ( 𝑥 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝐵 ) )
3	2	el2v1	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝐵 ) )
4	3	rexbidv	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 𝐵 ∈ [ 𝑥 ] 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ) )
5	1 4	bitr4d	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ [ 𝑥 ] 𝑅 ) )