Description: Equivalent of php without negation. (Contributed by Rohan Ridenour, 3-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rr-phpd.1 | ⊢ ( 𝜑 → 𝐴 ∈ ω ) | |
rr-phpd.2 | ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) | ||
rr-phpd.3 | ⊢ ( 𝜑 → 𝐴 ≈ 𝐵 ) | ||
Assertion | rr-phpd | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rr-phpd.1 | ⊢ ( 𝜑 → 𝐴 ∈ ω ) | |
2 | rr-phpd.2 | ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) | |
3 | rr-phpd.3 | ⊢ ( 𝜑 → 𝐴 ≈ 𝐵 ) | |
4 | 2 | adantr | ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ⊆ 𝐴 ) |
5 | simpr | ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 = 𝐵 ) | |
6 | 5 | neqcomd | ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐵 = 𝐴 ) |
7 | dfpss2 | ⊢ ( 𝐵 ⊊ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 ∧ ¬ 𝐵 = 𝐴 ) ) | |
8 | 4 6 7 | sylanbrc | ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ⊊ 𝐴 ) |
9 | php | ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐴 ≈ 𝐵 ) | |
10 | 1 8 9 | syl2an2r | ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 ≈ 𝐵 ) |
11 | 10 | ex | ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐵 → ¬ 𝐴 ≈ 𝐵 ) ) |
12 | 3 11 | mt4d | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |