![]() |
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 2010 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | sbcieg.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | sbciegf 3663 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1653 ∈ wcel 2157 [wsbc 3631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-12 2213 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-v 3385 df-sbc 3632 |
This theorem is referenced by: sbcie 3666 ralsng 4407 rexsng 4408 rabsnif 4445 ralrnmpt 6592 fpwwe2lem3 9741 nn1suc 11333 opfi1uzind 13528 mrcmndind 17678 fgcl 22007 cfinfil 22022 csdfil 22023 supfil 22024 fin1aufil 22061 ifeqeqx 29871 nn0min 30077 bnj1452 31629 cdlemk35s 36950 cdlemk39s 36952 cdlemk42 36954 2nn0ind 38283 zindbi 38284 |
Copyright terms: Public domain | W3C validator |