![]() |
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 2901 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) |
4 | 1, 3 | sylibr 233 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 Ⅎwnfc 2884 |
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-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 df-cleq 2725 df-clel 2811 df-nfc 2886 |
This theorem is referenced by: nfcsb1d 3917 nfcsbd 3920 nfcsbw 3921 nfifd 4558 nfunid 4915 nfopabd 5217 nfiotadw 6499 nfiotad 6501 nfriotadw 7373 nfriotad 7377 nfovd 7438 nfttrcld 9705 nfnegd 11455 nfxnegd 44151 nfintd 47718 nfiund 47719 nfiundg 47720 |
Copyright terms: Public domain | W3C validator |