| 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 1962. Version of r19.23 3259 with a disjoint variable 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 318 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) | |
| 2 | 1 | ralbii 3108 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑)) |
| 3 | r19.21v 3187 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
| 4 | dfrex2 3089 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 5 | 4 | imbi1i 351 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓)) |
| 6 | con1b 360 | . . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
| 7 | 5, 6 | bitr2i 278 | . 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
| 8 | 2, 3, 7 | 3bitri 299 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∀wral 3076 ∃wrex 3086 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-ex 1800 df-ral 3077 df-rex 3087 |
| This theorem is referenced by: ceqsralv 3494 ralxpxfr2d 3605 uniiunlem 4040 2reu4lem 4477 dfiin2g 4988 iunss 5002 iunssOLD 5003 replem 5238 ralxfr2d 5367 ssrel2 5757 idrefALT 6100 dfpo2 6283 funimass4 6931 fnssintima 7346 ralrnmpo 7535 imaeqalov 7635 ttrclss 9675 kmlem12 10118 fimaxre3 12138 gcdcllem1 16533 vdwmc2 17015 iunocv 21733 islindf4 21890 ovolgelb 25542 dyadmax 25660 itg2leub 25796 eqcuts2 27879 addsprop 28069 addsuniflem 28094 negsprop 28128 mulsprop 28223 mulsuniflem 28242 mpteleeOLD 29096 nmoubi 30975 nmopub 32111 nmfnleub 32128 sigaclcu2 34417 untuni 36059 elintfv 36115 heibor1lem 38308 ispsubsp2 40370 pmapglbx 40393 neik0pk1imk0 44623 2reuimp0 47708 |
| Copyright terms: Public domain | W3C validator |