![]() |
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 3077 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | iman 403 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
3 | 2 | ralbii 3097 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) |
4 | 1, 3 | xchbinxr 335 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∀wral 3065 ∃wrex 3074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3066 df-rex 3075 |
This theorem is referenced by: nrexralim 3135 ceqsralbv 3608 frpoind 6297 wfiOLD 6306 frind 9687 qsqueeze 13121 ncoprmgcdne1b 16527 elcls 22427 ist1-2 22701 haust1 22706 t1sep 22724 bwth 22764 1stccnp 22816 filufint 23274 fclscf 23379 pmltpc 24817 ovolgelb 24847 itg2seq 25110 radcnvlt1 25780 pntlem3 26960 nosupbnd1lem5 27063 noinfbnd1lem5 27078 umgr2edg1 28162 umgr2edgneu 28165 archiabl 32037 ordtconnlem1 32508 limsucncmpi 34920 matunitlindflem1 36077 ftc1anclem5 36158 clsk3nimkb 42319 |
Copyright terms: Public domain | W3C validator |