Metamath Proof Explorer

Theorem rexrnmpo

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 rexrnmpo ⊢ ∀ 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 2 notbid ⊢ z = C → ¬ φ ↔ ¬ ψ
4 1 3 ralrnmpo ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ z ∈ ran ⁡ F ¬ φ ↔ ∀ x ∈ A ∀ y ∈ B ¬ ψ
5 4 notbid ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ¬ ∀ z ∈ ran ⁡ F ¬ φ ↔ ¬ ∀ x ∈ A ∀ y ∈ B ¬ ψ
6 dfrex2 ⊢ ∃ z ∈ ran ⁡ F φ ↔ ¬ ∀ z ∈ ran ⁡ F ¬ φ
7 dfrex2 ⊢ ∃ y ∈ B ψ ↔ ¬ ∀ y ∈ B ¬ ψ
8 7 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B ψ ↔ ∃ x ∈ A ¬ ∀ y ∈ B ¬ ψ
9 rexnal ⊢ ∃ x ∈ A ¬ ∀ y ∈ B ¬ ψ ↔ ¬ ∀ x ∈ A ∀ y ∈ B ¬ ψ
10 8 9 bitri ⊢ ∃ x ∈ A ∃ y ∈ B ψ ↔ ¬ ∀ x ∈ A ∀ y ∈ B ¬ ψ
11 5 6 10 3bitr4g ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∃ z ∈ ran ⁡ F φ ↔ ∃ x ∈ A ∃ y ∈ B ψ