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 𝐹 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) )