Description: Condition for a restricted class abstraction to be empty. Version of rabeq0 using implicit substitution, which does not require ax-10 , ax-11 , ax-12 , but requires ax-8 . (Contributed by GG, 30-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rabeq0w.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | rabeq0w | ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabeq0w.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | eleq1w | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) | |
| 3 | 2 1 | anbi12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) |
| 4 | 3 | ab0w | ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = ∅ ↔ ∀ 𝑦 ¬ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) |
| 5 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } | |
| 6 | 5 | eqeq1i | ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ∅ ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = ∅ ) |
| 7 | raln | ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ∀ 𝑦 ¬ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) | |
| 8 | 4 6 7 | 3bitr4i | ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 ) |