![]() |
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 2904 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) |
4 | 1, 3 | sylibr 233 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 Ⅎwnfc 2887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-nf 1786 df-cleq 2728 df-clel 2814 df-nfc 2889 |
This theorem is referenced by: nfcsb1d 3878 nfcsbd 3881 nfcsbw 3882 nfifd 4515 nfunid 4871 nfopabd 5173 nfiotadw 6451 nfiotad 6453 nfriotadw 7321 nfriotad 7325 nfovd 7386 nfttrcld 9646 nfnegd 11396 nfxnegd 43666 nfintd 47108 nfiund 47109 nfiundg 47110 |
Copyright terms: Public domain | W3C validator |