|   | 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 1894 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | 
| 5 | 3, 2 | nfimd 1894 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜒 → 𝜓)) | 
| 6 | 4, 5 | nfand 1897 | . 2 ⊢ (𝜑 → Ⅎ𝑥((𝜓 → 𝜒) ∧ (𝜒 → 𝜓))) | 
| 7 | 1, 6 | nfxfrd 1854 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 Ⅎwnf 1783 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 | 
| This theorem is referenced by: nfbi 1903 nfeqd 2916 nfiotadw 6517 nfiotad 6519 iota2df 6548 axextnd 10631 axrepndlem1 10632 axrepndlem2 10633 axacndlem4 10650 axacndlem5 10651 axacnd 10652 axsepg2 35096 axsepg2ALT 35097 axextdist 35800 copsex2d 37140 cbveud 37373 wl-eudf 37573 wl-sb8eut 37579 wl-sb8eutv 37580 | 
| Copyright terms: Public domain | W3C validator |