Metamath Proof Explorer

Theorem dmqseqim2

Description: Lemma for erim2 . (Contributed by Peter Mazsa, 29-Dec-2021)

Ref Expression
Assertion dmqseqim2 ⊢ R ∈ V → Rel ⁡ R → dom ⁡ R / R = A → B ∈ ran ⁡ R ↔ B ∈ ⋃ A

Proof

Step Hyp Ref Expression
1 dmqseqim ⊢ R ∈ V → Rel ⁡ R → dom ⁡ R / R = A → ran ⁡ R = ⋃ A
2 eleq2 ⊢ ran ⁡ R = ⋃ A → B ∈ ran ⁡ R ↔ B ∈ ⋃ A
3 1 2 syl8 ⊢ R ∈ V → Rel ⁡ R → dom ⁡ R / R = A → B ∈ ran ⁡ R ↔ B ∈ ⋃ A