|   | 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 1941. Version of r19.23 3255 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 3092 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑)) | 
| 3 | r19.21v 3179 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | |
| 4 | dfrex2 3072 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 5 | 4 | imbi1i 349 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓)) | 
| 6 | con1b 358 | . . 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 206 ∀wral 3060 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: rexlimivOLD 3184 ceqsralv 3521 ralxpxfr2d 3645 uniiunlem 4086 2reu4lem 4521 dfiin2g 5031 iunss 5044 ralxfr2d 5409 ssrel2 5794 reliun 5825 idrefALT 6130 dfpo2 6315 funimass4 6972 fnssintima 7383 ralrnmpo 7573 imaeqalov 7673 ttrclss 9761 kmlem12 10203 fimaxre3 12215 gcdcllem1 16537 vdwmc2 17018 iunocv 21700 islindf4 21859 ovolgelb 25516 dyadmax 25634 itg2leub 25770 eqscut2 27852 addsprop 28010 addsuniflem 28035 negsprop 28068 mulsprop 28157 mulsuniflem 28176 mptelee 28911 nmoubi 30792 nmopub 31928 nmfnleub 31945 sigaclcu2 34122 untuni 35710 elintfv 35766 heibor1lem 37817 ispsubsp2 39749 pmapglbx 39772 neik0pk1imk0 44065 2reuimp0 47131 | 
| Copyright terms: Public domain | W3C validator |