![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > hbxfrbi | Structured version Visualization version GIF version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2869 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
hbxfrbi.1 | ⊢ (𝜑 ↔ 𝜓) |
hbxfrbi.2 | ⊢ (𝜓 → ∀𝑥𝜓) |
Ref | Expression |
---|---|
hbxfrbi | ⊢ (𝜑 → ∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbxfrbi.2 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | hbxfrbi.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | albii 1822 | . 2 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
4 | 1, 2, 3 | 3imtr4i 292 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 |
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 |
This theorem is referenced by: hbn1fw 2049 hbe1w 2052 hbe1 2140 hbsbw 2170 hbab1OLD 2724 hbab 2725 hbabg 2726 hbxfreq 2869 hbral 3294 bnj982 33430 bnj1095 33433 bnj1096 33434 bnj1276 33466 bnj594 33564 bnj1445 33696 hbra2VD 43216 |
Copyright terms: Public domain | W3C validator |