This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexrnmpt

Description: A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker rexrnmptw when possible. (Contributed by Mario Carneiro, 20-Aug-2015) (New usage is discouraged.)

Ref Expression
Hypotheses ralrnmpt.1 ⊢ F = x ∈ A ⟼ B
ralrnmpt.2 ⊢ y = B → ψ ↔ χ
Assertion rexrnmpt ⊢ ∀ x ∈ A B ∈ V → ∃ y ∈ ran ⁡ F ψ ↔ ∃ x ∈ A χ

Proof

Step Hyp Ref Expression
1 ralrnmpt.1 ⊢ F = x ∈ A ⟼ B
2 ralrnmpt.2 ⊢ y = B → ψ ↔ χ
3 2 notbid ⊢ y = B → ¬ ψ ↔ ¬ χ
4 1 3 ralrnmpt ⊢ ∀ x ∈ A B ∈ V → ∀ y ∈ ran ⁡ F ¬ ψ ↔ ∀ x ∈ A ¬ χ
5 4 notbid ⊢ ∀ x ∈ A B ∈ V → ¬ ∀ y ∈ ran ⁡ F ¬ ψ ↔ ¬ ∀ x ∈ A ¬ χ
6 dfrex2 ⊢ ∃ y ∈ ran ⁡ F ψ ↔ ¬ ∀ y ∈ ran ⁡ F ¬ ψ
7 dfrex2 ⊢ ∃ x ∈ A χ ↔ ¬ ∀ x ∈ A ¬ χ
8 5 6 7 3bitr4g ⊢ ∀ x ∈ A B ∈ V → ∃ y ∈ ran ⁡ F ψ ↔ ∃ x ∈ A χ