Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcie | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.) |
Ref | Expression |
---|---|
sbcie.1 | ⊢ 𝐴 ∈ V |
sbcie.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbcie | ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcie.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | sbcie.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbcieg 3809 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ∈ wcel 2110 Vcvv 3494 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3496 df-sbc 3772 |
This theorem is referenced by: rexopabb 5414 reuop 6143 tfinds2 7577 findcard2 8757 ac6sfi 8761 ac6num 9900 fpwwe 10067 nn1suc 11658 wrdind 14083 cjth 14461 fprodser 15302 prmind2 16028 joinlem 17620 meetlem 17634 mndind 17991 isghm 18357 islmod 19637 islindf 20955 fgcl 22485 cfinfil 22500 csdfil 22501 supfil 22502 fin1aufil 22539 quotval 24880 dfconngr1 27966 isconngr 27967 isconngr1 27968 wrdt2ind 30627 bnj62 31990 bnj610 32018 bnj976 32049 bnj106 32140 bnj125 32144 bnj154 32150 bnj155 32151 bnj526 32160 bnj540 32164 bnj591 32183 bnj609 32189 bnj893 32200 bnj1417 32313 soseq 33096 poimirlem27 34918 sdclem2 35016 fdc 35019 fdc1 35020 lshpkrlem3 36247 hdmap1fval 38931 hdmapfval 38962 rabren3dioph 39410 2nn0ind 39540 zindbi 39541 onfrALTlem5 40874 onfrALTlem5VD 41217 reupr 43683 |
Copyright terms: Public domain | W3C validator |