![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralbid | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3171. (Contributed by NM, 27-Jun-1998.) |
Ref | Expression |
---|---|
ralbid.1 | ⊢ Ⅎ𝑥𝜑 |
ralbid.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbid | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbid.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbid.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | adantr 482 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
4 | 1, 3 | ralbida 3252 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 Ⅎwnf 1786 ∈ 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 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-nf 1787 df-ral 3062 |
This theorem is referenced by: raleqbid 3329 sbcralt 3829 sbcrext 3830 riota5f 7343 zfrep6 7888 cnfcom3clem 9646 cplem2 9831 infxpenc2lem2 9961 acnlem 9989 lble 12112 fsuppmapnn0fiubex 13903 nosupbnd1 27078 noinfbnd1 27093 chirred 31379 rspc2daf 31439 aciunf1lem 31624 indexa 36238 riotasvd 37464 cdlemk36 39422 choicefi 43508 axccdom 43530 rexabsle 43740 infxrunb3rnmpt 43749 uzublem 43751 climf 43949 climf2 43993 limsupubuzlem 44039 cncficcgt0 44215 stoweidlem16 44343 stoweidlem18 44345 stoweidlem21 44348 stoweidlem29 44356 stoweidlem31 44358 stoweidlem36 44363 stoweidlem41 44368 stoweidlem44 44371 stoweidlem45 44372 stoweidlem51 44378 stoweidlem55 44382 stoweidlem59 44386 stoweidlem60 44387 issmfgelem 45096 smfpimcclem 45134 sprsymrelf 45773 |
Copyright terms: Public domain | W3C validator |