Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.23v | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.23v 1902. Version of r19.23 3022 with a dv condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
Ref | Expression |
---|---|
r19.23v | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con34b 306 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) | |
2 | 1 | ralbii 2980 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑)) |
3 | r19.21v 2960 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
4 | dfrex2 2996 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
5 | 4 | imbi1i 339 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓)) |
6 | con1b 348 | . . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
7 | 5, 6 | bitr2i 265 | . 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
8 | 2, 3, 7 | 3bitri 286 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∀wral 2912 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: rexlimiv 3027 ralxpxfr2d 3327 uniiunlem 3691 dfiin2g 4553 iunss 4561 ralxfr2d 4882 ssrel2 5210 reliun 5239 funimass4 6247 ralrnmpt2 6775 kmlem12 8983 fimaxre3 10970 gcdcllem1 15221 vdwmc2 15683 iunocv 20025 islindf4 20177 ovolgelb 23248 dyadmax 23366 itg2leub 23501 mptelee 25775 nmoubi 27627 nmopub 28767 nmfnleub 28784 sigaclcu2 30183 untuni 31586 dfpo2 31645 elintfv 31662 heibor1lem 33608 ispsubsp2 35032 pmapglbx 35055 neik0pk1imk0 38345 2reu4a 41189 |
Copyright terms: Public domain | W3C validator |