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 3202 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)) | |
2 | rsp 3202 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → (𝑦 ∈ 𝐵 → 𝜑)) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑))) |
4 | 3 | impd 411 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-ral 3140 |
This theorem is referenced by: ralcom2w 3360 ralcom2 3361 disjxiun 5054 solin 5491 mpocurryd 7924 cmncom 18852 cnmpt21 22207 cnmpt2t 22209 cnmpt22 22210 cnmptcom 22214 frgrwopreglem5ALT 28028 htthlem 28621 qsidomlem2 30883 cplgredgex 32264 prtlem14 35890 islptre 41776 sprsymrelfolem2 43532 |
Copyright terms: Public domain | W3C validator |