![]() |
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 3816 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 Vcvv 3475 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-sbc 3777 |
This theorem is referenced by: sbc2ie 3859 csbie 3928 rexopabb 5527 reuop 6289 tfinds2 7848 soseq 8140 findcard2 9160 findcard2OLD 9280 ac6sfi 9283 ac6num 10470 fpwwe 10637 nn1suc 12230 wrdind 14668 cjth 15046 fprodser 15889 prmind2 16618 joinlem 18332 meetlem 18346 mndind 18705 isghm 19086 islmod 20463 islindf 21351 fgcl 23364 cfinfil 23379 csdfil 23380 supfil 23381 fin1aufil 23418 quotval 25787 dfconngr1 29421 isconngr 29422 isconngr1 29423 wrdt2ind 32095 bnj62 33669 bnj610 33696 bnj976 33726 bnj106 33817 bnj125 33821 bnj154 33827 bnj155 33828 bnj526 33837 bnj540 33841 bnj591 33860 bnj609 33866 bnj893 33877 bnj1417 33990 poimirlem27 36453 sdclem2 36548 fdc 36551 fdc1 36552 lshpkrlem3 37920 hdmap1fval 40605 hdmapfval 40636 rabren3dioph 41486 2nn0ind 41617 zindbi 41618 onfrALTlem5 43236 onfrALTlem5VD 43579 reupr 46125 |
Copyright terms: Public domain | W3C validator |