![]() |
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 1915 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | sbcieg.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | sbciegf 3757 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∈ wcel 2111 [wsbc 3720 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-sbc 3721 |
This theorem is referenced by: sbcie 3760 2nreu 4349 reuprg0 4598 rabsnif 4619 ralrnmptw 6837 ralrnmpt 6839 fpwwe2lem3 10044 nn1suc 11647 opfi1uzind 13855 mndind 17984 fgcl 22483 cfinfil 22498 csdfil 22499 supfil 22500 fin1aufil 22537 ifeqeqx 30309 nn0min 30562 bnj1452 32434 cdlemk35s 38233 cdlemk39s 38235 cdlemk42 38237 2nn0ind 39886 zindbi 39887 prproropreud 44026 |
Copyright terms: Public domain | W3C validator |