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 3772 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | elex 3513 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V) | |
3 | 1, 2 | sylbi 218 | 1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 {cab 2799 Vcvv 3495 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3497 df-sbc 3772 |
This theorem is referenced by: sbccow 3794 sbcco 3797 sbc5 3799 sbcan 3820 sbcor 3821 sbcn1 3823 sbcim1 3824 sbcbi1 3829 sbcal 3832 sbcex2 3833 sbcel1v 3838 sbcel1vOLD 3839 sbcel21v 3841 sbcimdv 3842 sbcrext 3855 sbcreu 3858 spesbc 3864 csbprc 4357 sbcel12 4359 sbcne12 4363 sbcel2 4366 sbccsb2 4385 sbcbr123 5112 opelopabsb 5409 csbopab 5434 csbxp 5644 csbiota 6342 csbriota 7118 fi1uzind 13845 bj-csbprc 34124 sbccomieg 39270 |
Copyright terms: Public domain | W3C validator |