Metamath Proof Explorer

Theorem ralrnmpo

Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses rngop.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
ralrnmpo.2 ⊢ z = C → φ ↔ ψ
Assertion ralrnmpo ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ z ∈ ran ⁡ F φ ↔ ∀ x ∈ A ∀ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 ralrnmpo.2 ⊢ z = C → φ ↔ ψ
3 1 rnmpo ⊢ ran ⁡ F = w | ∃ x ∈ A ∃ y ∈ B w = C
4 3 raleqi ⊢ ∀ z ∈ ran ⁡ F φ ↔ ∀ z ∈ w | ∃ x ∈ A ∃ y ∈ B w = C φ
5 eqeq1 ⊢ w = z → w = C ↔ z = C
6 5 2rexbidv ⊢ w = z → ∃ x ∈ A ∃ y ∈ B w = C ↔ ∃ x ∈ A ∃ y ∈ B z = C
7 6 ralab ⊢ ∀ z ∈ w | ∃ x ∈ A ∃ y ∈ B w = C φ ↔ ∀ z ∃ x ∈ A ∃ y ∈ B z = C → φ
8 ralcom4 ⊢ ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ ↔ ∀ z ∀ x ∈ A ∃ y ∈ B z = C → φ
9 r19.23v ⊢ ∀ x ∈ A ∃ y ∈ B z = C → φ ↔ ∃ x ∈ A ∃ y ∈ B z = C → φ
10 9 albii ⊢ ∀ z ∀ x ∈ A ∃ y ∈ B z = C → φ ↔ ∀ z ∃ x ∈ A ∃ y ∈ B z = C → φ
11 8 10 bitr2i ⊢ ∀ z ∃ x ∈ A ∃ y ∈ B z = C → φ ↔ ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ
12 4 7 11 3bitri ⊢ ∀ z ∈ ran ⁡ F φ ↔ ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ
13 ralcom4 ⊢ ∀ y ∈ B ∀ z z = C → φ ↔ ∀ z ∀ y ∈ B z = C → φ
14 r19.23v ⊢ ∀ y ∈ B z = C → φ ↔ ∃ y ∈ B z = C → φ
15 14 albii ⊢ ∀ z ∀ y ∈ B z = C → φ ↔ ∀ z ∃ y ∈ B z = C → φ
16 13 15 bitri ⊢ ∀ y ∈ B ∀ z z = C → φ ↔ ∀ z ∃ y ∈ B z = C → φ
17 nfv ⊢ Ⅎ z ψ
18 17 2 ceqsalg ⊢ C ∈ V → ∀ z z = C → φ ↔ ψ
19 18 ralimi ⊢ ∀ y ∈ B C ∈ V → ∀ y ∈ B ∀ z z = C → φ ↔ ψ
20 ralbi ⊢ ∀ y ∈ B ∀ z z = C → φ ↔ ψ → ∀ y ∈ B ∀ z z = C → φ ↔ ∀ y ∈ B ψ
21 19 20 syl ⊢ ∀ y ∈ B C ∈ V → ∀ y ∈ B ∀ z z = C → φ ↔ ∀ y ∈ B ψ
22 16 21 bitr3id ⊢ ∀ y ∈ B C ∈ V → ∀ z ∃ y ∈ B z = C → φ ↔ ∀ y ∈ B ψ
23 22 ralimi ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ ↔ ∀ y ∈ B ψ
24 ralbi ⊢ ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ ↔ ∀ y ∈ B ψ → ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ ↔ ∀ x ∈ A ∀ y ∈ B ψ
25 23 24 syl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ x ∈ A ∀ z ∃ y ∈ B z = C → φ ↔ ∀ x ∈ A ∀ y ∈ B ψ
26 12 25 syl5bb ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ z ∈ ran ⁡ F φ ↔ ∀ x ∈ A ∀ y ∈ B ψ