![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexab | Structured version Visualization version GIF version |
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 Gino Giotto, 2-Nov-2024.) |
Ref | Expression |
---|---|
ralab.1 | ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexab | ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrex2 3074 | . . . 4 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒) | |
2 | ralab.1 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
3 | 2 | ralab 3688 | . . . 4 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒)) |
4 | 1, 3 | xchbinx 334 | . . 3 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒)) |
5 | imnang 1845 | . . 3 ⊢ (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) | |
6 | 4, 5 | xchbinx 334 | . 2 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) |
7 | df-ex 1783 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) | |
8 | 6, 7 | bitr4i 278 | 1 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 ∃wex 1782 {cab 2710 ∀wral 3062 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2711 df-ral 3063 df-rex 3072 |
This theorem is referenced by: 4sqlem12 16889 noinfno 27221 sleadd1 27472 addsuniflem 27484 addsasslem1 27486 addsasslem2 27487 mulsuniflem 27604 addsdilem1 27606 addsdilem2 27607 mulsasslem1 27618 mulsasslem2 27619 mblfinlem3 36527 mblfinlem4 36528 ismblfin 36529 itg2addnclem 36539 itg2addnc 36542 diophrex 41513 |
Copyright terms: Public domain | W3C validator |