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 1950. Version of r19.23 3223 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 319 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) | |
2 | 1 | ralbii 3078 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑)) |
3 | r19.21v 3088 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
4 | dfrex2 3151 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
5 | 4 | imbi1i 353 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓)) |
6 | con1b 362 | . . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
7 | 5, 6 | bitr2i 279 | . 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
8 | 2, 3, 7 | 3bitri 300 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∀wral 3051 ∃wrex 3052 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-ral 3056 df-rex 3057 |
This theorem is referenced by: rexlimiv 3189 ceqsralv 3435 ralxpxfr2d 3543 uniiunlem 3985 2reu4lem 4423 dfiin2g 4927 iunss 4940 ralxfr2d 5288 ssrel2 5641 reliun 5671 idrefALT 5958 funimass4 6755 ralrnmpo 7326 kmlem12 9740 fimaxre3 11743 gcdcllem1 16021 vdwmc2 16495 iunocv 20597 islindf4 20754 ovolgelb 24331 dyadmax 24449 itg2leub 24586 mptelee 26940 nmoubi 28807 nmopub 29943 nmfnleub 29960 sigaclcu2 31754 untuni 33317 fnssintima 33345 dfpo2 33392 elintfv 33408 eqscut2 33686 heibor1lem 35653 ispsubsp2 37446 pmapglbx 37469 neik0pk1imk0 41275 2reuimp0 44221 |
Copyright terms: Public domain | W3C validator |