![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alral | Structured version Visualization version GIF version |
Description: Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.) |
Ref | Expression |
---|---|
alral | ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ala1 1810 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | df-ral 3060 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | sylibr 234 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ∈ wcel 2106 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-ral 3060 |
This theorem is referenced by: abnex 7776 find 7918 brdom5 10567 brdom4 10568 hashgt23el 14460 prodeq2w 15943 rpnnen2lem12 16258 umgr2cycllem 35125 umgr2cycl 35126 elpotr 35763 fvineqsnf1 37393 fvineqsneq 37395 phpreu 37591 ordelordALTVD 44865 ssclaxsep 44947 rexrsb 47050 |
Copyright terms: Public domain | W3C validator |