| 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 1813 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 2 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 3 | 1, 2 | sylibr 234 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: abnex 7777 find 7917 brdom5 10569 brdom4 10570 hashgt23el 14463 prodeq2w 15946 rpnnen2lem12 16261 umgr2cycllem 35145 umgr2cycl 35146 elpotr 35782 fvineqsnf1 37411 fvineqsneq 37413 phpreu 37611 ordelordALTVD 44887 ssclaxsep 44999 rexrsb 47112 |
| Copyright terms: Public domain | W3C validator |