Theorem sbcel1v 3809

Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2402. (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 3754	. 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V)
2		elex 3474	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		dfsbcq2 3747	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵))
4		eleq1 2849	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		clelsb1 2888	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)
6	3, 4, 5	vtoclbg 3523	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7	1, 2, 6	pm5.21nii 380	1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 208  [wsb 2089   ∈ wcel 2141  Vcvv 3453  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-sbc 3745

This theorem is referenced by:  tfinds2  7840  filuni  23925  gropeld  29180  grstructeld  29181  f1od2  32871  esum2dlem  34350  bnj110  35117  f1omptsnlem  37794  relowlpssretop  37822  rdgeqoa  37828  minregex  44074  cotrclrcl  44282  frege70  44473  frege72  44475  frege91  44494  sbcoreleleq  45075  onfrALTlem4  45083  sbcoreleleqVD  45398  onfrALTlem4VD  45425  rspesbcd  45477