![]() |
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 3777 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
2 | elex 3482 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 {cab 2703 Vcvv 3462 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-sbc 3777 |
This theorem is referenced by: sbccow 3799 sbcco 3802 sbc5ALT 3805 sbcan 3829 sbcor 3830 sbcn1 3832 sbcim1 3833 sbcim1OLD 3834 sbcbi1 3838 sbcal 3840 sbcex2 3841 sbcel1v 3847 sbcel21v 3849 sbcimdvOLD 3851 sbcrext 3866 sbcreu 3869 spesbc 3875 csbprc 4411 sbcel12 4413 sbcne12 4417 sbcel2 4420 sbccsb2 4439 sbcbr123 5207 opelopabsb 5536 csbopab 5561 csbxp 5781 csbiota 6547 csbriota 7396 fi1uzind 14516 bj-csbprc 36616 sbccomieg 42450 |
Copyright terms: Public domain | W3C validator |