| 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 GG, 2-Nov-2024.) |
| Ref | Expression |
|---|---|
| ralab.1 | ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rexab | ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfrex2 3073 | . . . 4 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒) | |
| 2 | ralab.1 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | ralab 3697 | . . . 4 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒)) |
| 4 | 1, 3 | xchbinx 334 | . . 3 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒)) |
| 5 | imnang 1842 | . . 3 ⊢ (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) | |
| 6 | 4, 5 | xchbinx 334 | . 2 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) |
| 7 | df-ex 1780 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) | |
| 8 | 6, 7 | bitr4i 278 | 1 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 ∃wex 1779 {cab 2714 ∀wral 3061 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: 4sqlem12 16994 noinfno 27763 sleadd1 28022 addsuniflem 28034 addsasslem1 28036 addsasslem2 28037 mulsuniflem 28175 addsdilem1 28177 addsdilem2 28178 mulsasslem1 28189 mulsasslem2 28190 renegscl 28430 readdscl 28431 remulscl 28434 mblfinlem3 37666 mblfinlem4 37667 ismblfin 37668 itg2addnclem 37678 itg2addnc 37681 diophrex 42786 |
| Copyright terms: Public domain | W3C validator |