Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbcex | GIF version |
Description: By our definition of proper substitution, it can only be true if the substituted expression is a set. (Contributed by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
sbcex | ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc 2910 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | elex 2697 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 {cab 2125 Vcvv 2686 [wsbc 2909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-v 2688 df-sbc 2910 |
This theorem is referenced by: sbcco 2930 sbc5 2932 sbcan 2951 sbcor 2953 sbcn1 2956 sbcim1 2957 sbcbi1 2958 sbcal 2960 sbcex2 2962 sbcel1v 2971 sbcel21v 2973 sbcimdv 2974 sbcrext 2986 spesbc 2994 csbprc 3408 opelopabsb 4182 |
Copyright terms: Public domain | W3C validator |