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 3239 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | iman 402 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
3 | 2 | ralbii 3165 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) |
4 | 1, 3 | xchbinxr 336 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∀wral 3138 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-ral 3143 df-rex 3144 |
This theorem is referenced by: nrexralim 3266 wfi 6175 qsqueeze 12584 ncoprmgcdne1b 15984 elcls 21611 ist1-2 21885 haust1 21890 t1sep 21908 bwth 21948 1stccnp 22000 filufint 22458 fclscf 22563 pmltpc 23980 ovolgelb 24010 itg2seq 24272 radcnvlt1 24935 pntlem3 26113 umgr2edg1 26921 umgr2edgneu 26924 archiabl 30755 ordtconnlem1 31067 ceqsralv2 32854 frpoind 32978 frind 32983 nosupbnd1lem5 33110 limsucncmpi 33691 matunitlindflem1 34770 ftc1anclem5 34853 clsk3nimkb 40270 |
Copyright terms: Public domain | W3C validator |