![]() |
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 2889 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) |
4 | 1, 3 | sylibr 233 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 Ⅎwnfc 2876 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-nf 1779 df-cleq 2718 df-clel 2803 df-nfc 2878 |
This theorem is referenced by: nfcsb1d 3915 nfcsbd 3918 nfcsbw 3919 nfifd 4562 nfunid 4919 nfopabd 5221 nfiotadw 6509 nfiotad 6511 nfriotadw 7388 nfriotad 7392 nfovd 7453 nfttrcld 9753 nfnegd 11505 nfxnegd 45056 nfintd 48419 nfiund 48420 nfiundg 48421 |
Copyright terms: Public domain | W3C validator |