Metamath Proof Explorer

Theorem rexunirn

Description: Restricted existential quantification over the union of the range of a function. Cf. rexrn and eluni2 . (Contributed by Thierry Arnoux, 19-Sep-2017)

Ref Expression
Hypotheses rexunirn.1 ⊢ F = x ∈ A ⟼ B
rexunirn.2 ⊢ x ∈ A → B ∈ V
Assertion rexunirn ⊢ ∃ x ∈ A ∃ y ∈ B φ → ∃ y ∈ ⋃ ran ⁡ F φ

Proof

Step Hyp Ref Expression
1 rexunirn.1 ⊢ F = x ∈ A ⟼ B
2 rexunirn.2 ⊢ x ∈ A → B ∈ V
3 df-rex ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ x x ∈ A ∧ ∃ y ∈ B φ
4 19.42v ⊢ ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ x ∈ A ∧ ∃ y y ∈ B ∧ φ
5 df-rex ⊢ ∃ y ∈ B φ ↔ ∃ y y ∈ B ∧ φ
6 5 anbi2i ⊢ x ∈ A ∧ ∃ y ∈ B φ ↔ x ∈ A ∧ ∃ y y ∈ B ∧ φ
7 4 6 bitr4i ⊢ ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ x ∈ A ∧ ∃ y ∈ B φ
8 7 exbii ⊢ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ ∃ x x ∈ A ∧ ∃ y ∈ B φ
9 3 8 bitr4i ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ
10 1 elrnmpt1 ⊢ x ∈ A ∧ B ∈ V → B ∈ ran ⁡ F
11 2 10 mpdan ⊢ x ∈ A → B ∈ ran ⁡ F
12 eleq2 ⊢ b = B → y ∈ b ↔ y ∈ B
13 12 anbi1d ⊢ b = B → y ∈ b ∧ φ ↔ y ∈ B ∧ φ
14 13 rspcev ⊢ B ∈ ran ⁡ F ∧ y ∈ B ∧ φ → ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
15 11 14 sylan ⊢ x ∈ A ∧ y ∈ B ∧ φ → ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
16 r19.41v ⊢ ∃ b ∈ ran ⁡ F y ∈ b ∧ φ ↔ ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
17 15 16 sylib ⊢ x ∈ A ∧ y ∈ B ∧ φ → ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
18 17 eximi ⊢ ∃ y x ∈ A ∧ y ∈ B ∧ φ → ∃ y ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
19 df-rex ⊢ ∃ y ∈ ⋃ ran ⁡ F φ ↔ ∃ y y ∈ ⋃ ran ⁡ F ∧ φ
20 eluni2 ⊢ y ∈ ⋃ ran ⁡ F ↔ ∃ b ∈ ran ⁡ F y ∈ b
21 20 anbi1i ⊢ y ∈ ⋃ ran ⁡ F ∧ φ ↔ ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
22 21 exbii ⊢ ∃ y y ∈ ⋃ ran ⁡ F ∧ φ ↔ ∃ y ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
23 19 22 bitri ⊢ ∃ y ∈ ⋃ ran ⁡ F φ ↔ ∃ y ∃ b ∈ ran ⁡ F y ∈ b ∧ φ
24 18 23 sylibr ⊢ ∃ y x ∈ A ∧ y ∈ B ∧ φ → ∃ y ∈ ⋃ ran ⁡ F φ
25 24 exlimiv ⊢ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ → ∃ y ∈ ⋃ ran ⁡ F φ
26 9 25 sylbi ⊢ ∃ x ∈ A ∃ y ∈ B φ → ∃ y ∈ ⋃ ran ⁡ F φ