![]() |
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 3245 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)) | |
2 | rsp 3245 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → (𝑦 ∈ 𝐵 → 𝜑)) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑))) |
4 | 3 | impd 412 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3062 |
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 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3063 |
This theorem is referenced by: ralcom2 3374 disjxiun 5146 mpocurryd 8254 cmncom 19666 cnmpt21 23175 cnmpt2t 23177 cnmpt22 23178 cnmptcom 23182 frgrwopreglem5ALT 29575 htthlem 30170 qsidomlem2 32572 cplgredgex 34111 disjlem14 37668 prtlem14 37744 islptre 44335 sprsymrelfolem2 46161 |
Copyright terms: Public domain | W3C validator |