|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > rsp2 | Structured version Visualization version GIF version | ||
| Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997.) | 
| Ref | Expression | 
|---|---|
| rsp2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | rsp 3246 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)) | |
| 2 | rsp 3246 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → (𝑦 ∈ 𝐵 → 𝜑)) | |
| 3 | 1, 2 | syl6 35 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑))) | 
| 4 | 3 | impd 410 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 ∀wral 3060 | 
| 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-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-ral 3061 | 
| This theorem is referenced by: ralcom2 3376 disjxiun 5139 mpocurryd 8295 cmncom 19817 cnmpt21 23680 cnmpt2t 23682 cnmpt22 23683 cnmptcom 23687 frgrwopreglem5ALT 30342 htthlem 30937 qsidomlem2 33482 cplgredgex 35127 disjlem14 38800 prtlem14 38876 islptre 45639 sprsymrelfolem2 47485 | 
| Copyright terms: Public domain | W3C validator |