![]() |
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 1816 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | sylibr 233 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ral 3062 |
This theorem is referenced by: abnex 7692 find 7834 findOLD 7835 brdom5 10470 brdom4 10471 hashgt23el 14330 prodeq2w 15800 rpnnen2lem12 16112 umgr2cycllem 33791 umgr2cycl 33792 elpotr 34412 fvineqsnf1 35927 fvineqsneq 35929 phpreu 36108 ordelordALTVD 43237 rexrsb 45418 |
Copyright terms: Public domain | W3C validator |