|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > spc2gv | Structured version Visualization version GIF version | ||
| Description: Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.) | 
| Ref | Expression | 
|---|---|
| spc2egv.1 | ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| spc2gv | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | spc2egv.1 | . . . . 5 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | notbid 318 | . . . 4 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (¬ 𝜑 ↔ ¬ 𝜓)) | 
| 3 | 2 | spc2egv 3598 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝜓 → ∃𝑥∃𝑦 ¬ 𝜑)) | 
| 4 | 2nalexn 1827 | . . 3 ⊢ (¬ ∀𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦 ¬ 𝜑) | |
| 5 | 3, 4 | imbitrrdi 252 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝜓 → ¬ ∀𝑥∀𝑦𝜑)) | 
| 6 | 5 | con4d 115 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1537 = wceq 1539 ∃wex 1778 ∈ wcel 2107 | 
| 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 ax-6 1966 ax-7 2006 ax-8 2109 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-clel 2815 | 
| This theorem is referenced by: rspc2gv 3631 trel 5267 elovmpo 7679 seqf1olem2 14084 seqf1o 14085 fi1uzind 14547 brfi1indALT 14550 pslem 18618 cnmpt12 23676 cnmpt22 23683 mclsppslem 35589 mbfresfi 37674 lpolconN 41490 ismrcd2 42715 ismrc 42717 euendfunc 49184 | 
| Copyright terms: Public domain | W3C validator |