![]() |
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 3071 | . . . 4 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒) | |
2 | ralab.1 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
3 | 2 | ralab 3700 | . . . 4 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒)) |
4 | 1, 3 | xchbinx 334 | . . 3 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒)) |
5 | imnang 1839 | . . 3 ⊢ (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) | |
6 | 4, 5 | xchbinx 334 | . 2 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) |
7 | df-ex 1777 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒)) | |
8 | 6, 7 | bitr4i 278 | 1 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1535 ∃wex 1776 {cab 2712 ∀wral 3059 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-ral 3060 df-rex 3069 |
This theorem is referenced by: 4sqlem12 16990 noinfno 27778 sleadd1 28037 addsuniflem 28049 addsasslem1 28051 addsasslem2 28052 mulsuniflem 28190 addsdilem1 28192 addsdilem2 28193 mulsasslem1 28204 mulsasslem2 28205 renegscl 28445 readdscl 28446 remulscl 28449 mblfinlem3 37646 mblfinlem4 37647 ismblfin 37648 itg2addnclem 37658 itg2addnc 37661 diophrex 42763 |
Copyright terms: Public domain | W3C validator |