Theorem sbcex 3719

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.)

Assertion

Ref	Expression
sbcex	⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)

Proof of Theorem sbcex

Step	Hyp	Ref	Expression
1		df-sbc 3710	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		elex 3455	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V)
3	1, 2	sylbi 218	1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)

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