![]() |
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 3254 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 3094 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑)) |
3 | r19.21v 3180 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
4 | dfrex2 3074 | . . . 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 3062 ∃wrex 3071 |
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 3063 df-rex 3072 |
This theorem is referenced by: rexlimivOLD 3185 ceqsralv 3514 ralxpxfr2d 3635 uniiunlem 4085 2reu4lem 4526 dfiin2g 5036 iunss 5049 ralxfr2d 5409 ssrel2 5786 reliun 5817 idrefALT 6113 dfpo2 6296 funimass4 6957 fnssintima 7359 ralrnmpo 7547 imaeqalov 7646 ttrclss 9715 kmlem12 10156 fimaxre3 12160 gcdcllem1 16440 vdwmc2 16912 iunocv 21234 islindf4 21393 ovolgelb 24997 dyadmax 25115 itg2leub 25252 eqscut2 27307 addsprop 27460 addsuniflem 27484 negsprop 27509 mulsprop 27586 mulsuniflem 27604 mptelee 28153 nmoubi 30025 nmopub 31161 nmfnleub 31178 sigaclcu2 33118 untuni 34678 elintfv 34736 heibor1lem 36677 ispsubsp2 38617 pmapglbx 38640 neik0pk1imk0 42798 2reuimp0 45822 |
Copyright terms: Public domain | W3C validator |