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 3170 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | iman 402 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
3 | 2 | ralbii 3092 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ¬ (𝜑 ∧ ¬ 𝜓)) |
4 | 1, 3 | xchbinxr 335 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∀wral 3064 ∃wrex 3065 |
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 397 df-ex 1783 df-ral 3069 df-rex 3070 |
This theorem is referenced by: nrexralim 3193 frpoind 6245 wfiOLD 6254 frind 9508 qsqueeze 12935 ncoprmgcdne1b 16355 elcls 22224 ist1-2 22498 haust1 22503 t1sep 22521 bwth 22561 1stccnp 22613 filufint 23071 fclscf 23176 pmltpc 24614 ovolgelb 24644 itg2seq 24907 radcnvlt1 25577 pntlem3 26757 umgr2edg1 27578 umgr2edgneu 27581 archiabl 31452 ordtconnlem1 31874 ceqsralv2 33670 nosupbnd1lem5 33915 noinfbnd1lem5 33930 limsucncmpi 34634 matunitlindflem1 35773 ftc1anclem5 35854 clsk3nimkb 41650 |
Copyright terms: Public domain | W3C validator |