![]() |
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.) Avoid ax-10 2139, ax-12 2175. (Revised by GG, 12-Oct-2024.) |
Ref | Expression |
---|---|
sbcieg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbcieg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc 3792 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | sbcieg.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | elabg 3677 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
4 | 1, 3 | bitrid 283 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∈ wcel 2106 {cab 2712 [wsbc 3791 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-sbc 3792 |
This theorem is referenced by: sbcie 3835 2nreu 4450 reuprg0 4707 rabsnif 4728 ralrnmptw 7114 ralrnmpt 7116 fpwwe2lem3 10671 nn1suc 12286 opfi1uzind 14547 mndind 18854 fgcl 23902 cfinfil 23917 csdfil 23918 supfil 23919 fin1aufil 23956 ifeqeqx 32563 nn0min 32827 bnj1452 35045 cdlemk35s 40920 cdlemk39s 40922 cdlemk42 40924 2nn0ind 42934 zindbi 42935 prproropreud 47434 |
Copyright terms: Public domain | W3C validator |