Theorem sbcex 3753

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 3744	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		elex 3475	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V)
3	1, 2	sylbi 220	1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  {cab 2740  Vcvv 3454  [wsbc 3743

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-sbc 3744

This theorem is used by:  sbccow  3766  sbcco  3769  sbc5ALT  3772  sbcan  3792  sbcor  3793  sbcn1  3795  sbcim1  3796  sbcbi1  3800  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbcel21v  3810  sbccomlem  3821  sbcrext  3825  sbcreu  3828  spesbc  3834  csbprc  4373  sbcel12  4375  sbcne12  4379  sbcel2  4382  sbccsb2  4401  sbcbr123  5164  opelopabsb  5513  csbopab  5539  csbxp  5761  csbiota  6529  csbriota  7384  fi1uzind  14551  bj-csbprc  37573  sbccomieg  43548