| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rexanali | Structured version Visualization version GIF version | ||
| Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.) |
| Ref | Expression |
|---|---|
| rexanali | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfrex2 3073 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) | |
| 2 | iman 401 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
| 3 | 2 | ralbii 3093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) |
| 4 | 1, 3 | xchbinxr 335 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: nrexralim 3137 ceqsralbv 3657 frpoind 6363 wfiOLD 6372 frind 9790 qsqueeze 13243 ncoprmgcdne1b 16687 elcls 23081 ist1-2 23355 haust1 23360 t1sep 23378 bwth 23418 1stccnp 23470 filufint 23928 fclscf 24033 pmltpc 25485 ovolgelb 25515 itg2seq 25777 radcnvlt1 26461 pntlem3 27653 nosupbnd1lem5 27757 noinfbnd1lem5 27772 umgr2edg1 29228 umgr2edgneu 29231 archiabl 33205 ordtconnlem1 33923 limsucncmpi 36446 matunitlindflem1 37623 ftc1anclem5 37704 clsk3nimkb 44053 |
| Copyright terms: Public domain | W3C validator |