| 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 3178. (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 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
| 4 | 1, 3 | ralbida 3270 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1783 ∈ 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 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 df-ral 3062 |
| This theorem is referenced by: raleqbid 3356 sbcralt 3872 sbcrext 3873 riota5f 7416 zfrep6 7979 cnfcom3clem 9745 cplem2 9930 infxpenc2lem2 10060 acnlem 10088 lble 12220 fsuppmapnn0fiubex 14033 nosupbnd1 27759 noinfbnd1 27774 chirred 32414 rspc2daf 32485 aciunf1lem 32672 indexa 37740 riotasvd 38957 cdlemk36 40915 modelaxreplem3 44997 choicefi 45205 axccdom 45227 rexabsle 45430 infxrunb3rnmpt 45439 uzublem 45441 climf 45637 climf2 45681 limsupubuzlem 45727 cncficcgt0 45903 stoweidlem16 46031 stoweidlem18 46033 stoweidlem21 46036 stoweidlem29 46044 stoweidlem31 46046 stoweidlem36 46051 stoweidlem41 46056 stoweidlem44 46059 stoweidlem45 46060 stoweidlem51 46066 stoweidlem55 46070 stoweidlem59 46074 stoweidlem60 46075 issmfgelem 46784 smfpimcclem 46822 sprsymrelf 47482 |
| Copyright terms: Public domain | W3C validator |