Description: Duplicate version of ralima . (Contributed by Scott Fenton, 27-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | imaeqsexvOLD.1 | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) ) | |
Assertion | imaeqsalvOLD | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaeqsexvOLD.1 | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) ) | |
2 | 1 | notbid | ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
3 | 2 | imaeqsexvOLD | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) ¬ 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ¬ 𝜓 ) ) |
4 | 3 | notbid | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ¬ ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) ¬ 𝜑 ↔ ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜓 ) ) |
5 | dfral2 | ⊢ ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ¬ ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) ¬ 𝜑 ) | |
6 | dfral2 | ⊢ ( ∀ 𝑦 ∈ 𝐵 𝜓 ↔ ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜓 ) | |
7 | 4 5 6 | 3bitr4g | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) ) |