![]() |
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 3243 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)) | |
2 | rsp 3243 | . . 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 2105 ∀wral 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-12 2170 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-ral 3061 |
This theorem is referenced by: ralcom2 3372 disjxiun 5145 mpocurryd 8260 cmncom 19714 cnmpt21 23495 cnmpt2t 23497 cnmpt22 23498 cnmptcom 23502 frgrwopreglem5ALT 30009 htthlem 30604 qsidomlem2 33013 cplgredgex 34576 disjlem14 38134 prtlem14 38210 islptre 44796 sprsymrelfolem2 46622 |
Copyright terms: Public domain | W3C validator |