Theorem sbcnel12g 3803

Description: Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)

Assertion

Ref	Expression
sbcnel12g	|- ( A e. V -> ( [. A / x ]. B e/ C <-> [_ A / x ]_ B e/ [_ A / x ]_ C ) )

Proof of Theorem sbcnel12g

Step	Hyp	Ref	Expression
1		sbcng 3341	. 2 |- ( A e. V -> ( [. A / x ]. -. B e. C <-> -. [. A / x ]. B e. C ) )
2		df-nel 2622	. . 3 |- ( B e/ C <-> -. B e. C )
3	2	sbcbii 3356	. 2 |- ( [. A / x ]. B e/ C <-> [. A / x ]. -. B e. C )
4		df-nel 2622	. . 3 |- ( [_ A / x ]_ B e/ [_ A / x ]_ C <-> -. [_ A / x ]_ B e. [_ A / x ]_ C )
5		sbcel12 3801	. . 3 |- ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )
6	4, 5	xchbinxr 313	. 2 |- ( [_ A / x ]_ B e/ [_ A / x ]_ C <-> -. [. A / x ]. B e. C )
7	1, 3, 6	3bitr4g 292	1 |- ( A e. V -> ( [. A / x ]. B e/ C <-> [_ A / x ]_ B e/ [_ A / x ]_ C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   e. wcel 1869   e/ wnel 2620   [.wsbc 3300   [_csb 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-nel 2622  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-in 3444  df-ss 3451  df-nul 3763

This theorem is referenced by:  rusbcALT  36654