| 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 2178, ax-12 2215. (Revised by GG, 12-Oct-2024.) |
| Ref | Expression |
|---|---|
| sbcieg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| sbcieg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-sbc 3748 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
| 2 | sbcieg.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | elabg 3638 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
| 4 | 1, 3 | bitrid 286 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 = wceq 1563 ∈ wcel 2145 {cab 2743 [wsbc 3747 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-tru 1566 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-sbc 3748 |
| This theorem is referenced by: sbcie 3788 2nreu 4401 reuprg0 4664 rabsnif 4685 ralrnmptw 7079 ralrnmpt 7081 fpwwe2lem3 10606 nn1suc 12243 opfi1uzind 14536 mndind 18875 fgcl 23992 cfinfil 24007 csdfil 24008 supfil 24009 fin1aufil 24046 ifeqeqx 32794 nn0min 33073 bnj1452 35352 cdlemk35s 41568 cdlemk39s 41570 cdlemk42 41572 2nn0ind 43529 zindbi 43530 prproropreud 48114 |
| Copyright terms: Public domain | W3C validator |