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 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) |