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

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
ralrnmpo.2 ⊢ ( 𝑧 = 𝐶 → ( 𝜑 ↔ 𝜓 ) )
Assertion rexrnmpo ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ∃ 𝑧 ∈ ran 𝐹 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 ralrnmpo.2 ⊢ ( 𝑧 = 𝐶 → ( 𝜑 ↔ 𝜓 ) )
3 2 notbid ⊢ ( 𝑧 = 𝐶 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
4 1 3 ralrnmpo ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ∀ 𝑧 ∈ ran 𝐹 ¬ 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) )
5 4 notbid ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ¬ ∀ 𝑧 ∈ ran 𝐹 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) )
6 dfrex2 ⊢ ( ∃ 𝑧 ∈ ran 𝐹 𝜑 ↔ ¬ ∀ 𝑧 ∈ ran 𝐹 ¬ 𝜑 )
7 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 )
8 7 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 )
9 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 )
10 8 9 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 )
11 5 6 10 3bitr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ∃ 𝑧 ∈ ran 𝐹 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) )