![]() |
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 1946. Version of r19.23 3238 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 316 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) | |
2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑)) |
3 | r19.21v 3173 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
4 | dfrex2 3073 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
5 | 4 | imbi1i 350 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓)) |
6 | con1b 359 | . . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
7 | 5, 6 | bitr2i 276 | . 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
8 | 2, 3, 7 | 3bitri 297 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wral 3061 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3062 df-rex 3071 |
This theorem is referenced by: rexlimivOLD 3178 ceqsralv 3482 ralxpxfr2d 3597 uniiunlem 4045 2reu4lem 4484 dfiin2g 4993 iunss 5006 ralxfr2d 5366 ssrel2 5742 reliun 5773 idrefALT 6066 dfpo2 6249 funimass4 6908 fnssintima 7308 ralrnmpo 7495 imaeqalov 7594 ttrclss 9661 kmlem12 10102 fimaxre3 12106 gcdcllem1 16384 vdwmc2 16856 iunocv 21101 islindf4 21260 ovolgelb 24860 dyadmax 24978 itg2leub 25115 eqscut2 27167 addsprop 27310 addsunif 27332 negsprop 27355 mptelee 27886 nmoubi 29756 nmopub 30892 nmfnleub 30909 sigaclcu2 32776 untuni 34337 elintfv 34395 heibor1lem 36314 ispsubsp2 38255 pmapglbx 38278 neik0pk1imk0 42407 2reuimp0 45432 |
Copyright terms: Public domain | W3C validator |