|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nfcxfrd | Structured version Visualization version GIF version | ||
| Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) | 
| Ref | Expression | 
|---|---|
| nfcxfr.1 | ⊢ 𝐴 = 𝐵 | 
| nfcxfrd.2 | ⊢ (𝜑 → Ⅎ𝑥𝐵) | 
| Ref | Expression | 
|---|---|
| nfcxfrd | ⊢ (𝜑 → Ⅎ𝑥𝐴) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nfcxfrd.2 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
| 2 | nfcxfr.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
| 3 | 2 | nfceqi 2902 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) | 
| 4 | 1, 3 | sylibr 234 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 Ⅎwnfc 2890 | 
| 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-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 df-cleq 2729 df-clel 2816 df-nfc 2892 | 
| This theorem is referenced by: nfcsb1d 3921 nfcsbd 3924 nfcsbw 3925 nfifd 4555 nfunid 4913 nfopabd 5211 nfiotadw 6517 nfiotad 6519 nfriotadw 7396 nfriotad 7399 nfovd 7460 nfttrcld 9750 nfnegd 11503 nfxnegd 45452 nfintd 49192 nfiund 49193 nfiundg 49194 | 
| Copyright terms: Public domain | W3C validator |