Description: Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019) (Proof shortened by Wolf Lammen, 25-Nov-2019) Definitial form. (Revised by Wolf Lammen, 5-Mar-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nabbib | ⊢ ( { 𝑥 ∣ 𝜑 } ≠ { 𝑥 ∣ 𝜓 } ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ne | ⊢ ( { 𝑥 ∣ 𝜑 } ≠ { 𝑥 ∣ 𝜓 } ↔ ¬ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ) | |
| 2 | exnal | ⊢ ( ∃ 𝑥 ¬ ( 𝜑 ↔ 𝜓 ) ↔ ¬ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) | |
| 3 | xor3 | ⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) ) | |
| 4 | 3 | exbii | ⊢ ( ∃ 𝑥 ¬ ( 𝜑 ↔ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ) |
| 5 | 2 4 | bitr3i | ⊢ ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ) |
| 6 | abbib | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) | |
| 7 | 5 6 | xchnxbir | ⊢ ( ¬ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ) |
| 8 | 1 7 | bitri | ⊢ ( { 𝑥 ∣ 𝜑 } ≠ { 𝑥 ∣ 𝜓 } ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ) |