![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfbid | Structured version Visualization version GIF version |
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ↔ 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |
Ref | Expression |
---|---|
nfbid.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
nfbid.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
Ref | Expression |
---|---|
nfbid | ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi2 474 | . 2 ⊢ ((𝜓 ↔ 𝜒) ↔ ((𝜓 → 𝜒) ∧ (𝜒 → 𝜓))) | |
2 | nfbid.1 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
3 | nfbid.2 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
4 | 2, 3 | nfimd 1892 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
5 | 3, 2 | nfimd 1892 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜒 → 𝜓)) |
6 | 4, 5 | nfand 1895 | . 2 ⊢ (𝜑 → Ⅎ𝑥((𝜓 → 𝜒) ∧ (𝜒 → 𝜓))) |
7 | 1, 6 | nfxfrd 1851 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nfbi 1901 nfeqd 2914 nfiotadw 6519 nfiotad 6521 iota2df 6550 axextnd 10629 axrepndlem1 10630 axrepndlem2 10631 axacndlem4 10648 axacndlem5 10649 axacnd 10650 axsepg2 35075 axsepg2ALT 35076 axextdist 35781 copsex2d 37122 cbveud 37355 wl-eudf 37553 wl-sb8eut 37559 wl-sb8eutv 37560 |
Copyright terms: Public domain | W3C validator |