|   | 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 2871 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 1818 | . 2 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) | 
| 4 | 1, 2, 3 | 3imtr4i 292 | 1 ⊢ (𝜑 → ∀𝑥𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1537 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 | 
| This theorem is referenced by: hbn1fw 2044 hbe1w 2047 hbe1 2142 hbsbwOLD 2171 hbab1OLD 2723 hbab 2724 hbabg 2725 hbxfreq 2871 hbral 3307 bnj982 34793 bnj1095 34796 bnj1096 34797 bnj1276 34829 bnj594 34927 bnj1445 35059 hbra2VD 44885 | 
| Copyright terms: Public domain | W3C validator |