Theorem sbcel1v 3831

Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2376. (Revised by Wolf Lammen, 30-Apr-2023.)

Assertion

Ref	Expression
sbcel1v	⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem sbcel1v

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbcex 3775	. 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V)
2		elex 3480	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		dfsbcq2 3768	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵))
4		eleq1 2822	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		clelsb1 2861	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)
6	3, 4, 5	vtoclbg 3536	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7	1, 2, 6	pm5.21nii 378	1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 206  [wsb 2064   ∈ wcel 2108  Vcvv 3459  [wsbc 3765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-sbc 3766

This theorem is referenced by:  tfinds2  7859  filuni  23823  gropeld  29012  grstructeld  29013  f1od2  32698  esum2dlem  34123  bnj110  34889  f1omptsnlem  37354  relowlpssretop  37382  rdgeqoa  37388  minregex  43558  cotrclrcl  43766  frege70  43957  frege72  43959  frege91  43978  sbcoreleleq  44560  onfrALTlem4  44568  sbcoreleleqVD  44883  onfrALTlem4VD  44910  rspesbcd  44962