![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcieg | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
sbcieg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbcieg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1995 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | sbcieg.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | sbciegf 3619 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1631 ∈ wcel 2145 [wsbc 3587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-v 3353 df-sbc 3588 |
This theorem is referenced by: sbcie 3622 ralsng 4356 rexsng 4357 rabsnif 4394 ralrnmpt 6511 fpwwe2lem3 9657 nn1suc 11243 opfi1uzind 13485 mrcmndind 17574 fgcl 21902 cfinfil 21917 csdfil 21918 supfil 21919 fin1aufil 21956 ifeqeqx 29699 nn0min 29907 bnj1452 31458 cdlemk35s 36746 cdlemk39s 36748 cdlemk42 36750 2nn0ind 38036 zindbi 38037 trsbcVD 39635 |
Copyright terms: Public domain | W3C validator |