Description: Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ralima.x | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) ) | |
Assertion | rexima | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralima.x | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) ) | |
2 | 1 | notbid | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
3 | 2 | ralima | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) ) |
4 | 3 | notbid | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ¬ ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) ) |
5 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ¬ ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) ¬ 𝜑 ) | |
6 | dfrex2 | ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) | |
7 | 4 5 6 | 3bitr4g | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) |