Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014) (Revised by Mario Carneiro, 3-Sep-2015) Reduce axiom usage. (Revised by GG, 2-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ralab.1 | ⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | rexab | ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜒 ↔ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralab.1 | ⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜒 ↔ ¬ ∀ 𝑥 ∈ { 𝑦 ∣ 𝜑 } ¬ 𝜒 ) | |
| 3 | 1 | ralab | ⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜑 } ¬ 𝜒 ↔ ∀ 𝑥 ( 𝜓 → ¬ 𝜒 ) ) |
| 4 | 2 3 | xchbinx | ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜒 ↔ ¬ ∀ 𝑥 ( 𝜓 → ¬ 𝜒 ) ) |
| 5 | imnang | ⊢ ( ∀ 𝑥 ( 𝜓 → ¬ 𝜒 ) ↔ ∀ 𝑥 ¬ ( 𝜓 ∧ 𝜒 ) ) | |
| 6 | 4 5 | xchbinx | ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜒 ↔ ¬ ∀ 𝑥 ¬ ( 𝜓 ∧ 𝜒 ) ) |
| 7 | df-ex | ⊢ ( ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ↔ ¬ ∀ 𝑥 ¬ ( 𝜓 ∧ 𝜒 ) ) | |
| 8 | 6 7 | bitr4i | ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜒 ↔ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) |