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 3152 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | iman 405 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
3 | 2 | ralbii 3080 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) |
4 | 1, 3 | xchbinxr 338 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∀wral 3053 ∃wrex 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-ral 3058 df-rex 3059 |
This theorem is referenced by: nrexralim 3176 wfi 6162 qsqueeze 12677 ncoprmgcdne1b 16091 elcls 21824 ist1-2 22098 haust1 22103 t1sep 22121 bwth 22161 1stccnp 22213 filufint 22671 fclscf 22776 pmltpc 24202 ovolgelb 24232 itg2seq 24495 radcnvlt1 25165 pntlem3 26345 umgr2edg1 27153 umgr2edgneu 27156 archiabl 31029 ordtconnlem1 31446 ceqsralv2 33243 frpoind 33383 frind 33391 nosupbnd1lem5 33556 noinfbnd1lem5 33571 limsucncmpi 34272 matunitlindflem1 35396 ftc1anclem5 35477 clsk3nimkb 41196 |
Copyright terms: Public domain | W3C validator |