![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcex | Structured version Visualization version 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 3710 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | elex 3455 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V) | |
3 | 1, 2 | sylbi 218 | 1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 {cab 2775 Vcvv 3437 [wsbc 3709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-v 3439 df-sbc 3710 |
This theorem is referenced by: sbcco 3732 sbc5 3734 sbcan 3753 sbcor 3754 sbcn1 3756 sbcim1 3757 sbcbi1 3762 sbcal 3765 sbcex2 3766 sbcel1v 3771 sbcel1vOLD 3772 sbcel21v 3774 sbcimdv 3775 sbcrext 3788 sbcreu 3791 spesbc 3797 csbprc 4282 sbcel12 4284 sbcne12 4288 sbcel2 4291 sbccsb2 4305 sbcbr123 5020 opelopabsb 5312 csbopab 5335 csbxp 5541 csbiota 6223 csbriota 6994 fi1uzind 13706 bj-csbprc 33807 sbccomieg 38900 |
Copyright terms: Public domain | W3C validator |