Theorem sbcel1v 3810

Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2404. (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 3755	. 2 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 → 𝐴 ∈ V)
2		elex 3476	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3		dfsbcq2 3748	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑥 ∈ 𝐵))
4		eleq1 2851	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		clelsb1 2890	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)
6	3, 4, 5	vtoclbg 3525	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7	1, 2, 6	pm5.21nii 381	1 ⊢ ([𝐴 / 𝑥]𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:   ↔ wb 209  [wsb 2096   ∈ wcel 2143  Vcvv 3455  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-sbc 3746

This theorem is referenced by:  tfinds2  7861  filuni  24023  gropeld  29364  grstructeld  29365  f1od2  33045  esum2dlem  34463  bnj110  35227  f1omptsnlem  37963  relowlpssretop  37991  rdgeqoa  37997  minregex  44243  cotrclrcl  44451  frege70  44642  frege72  44644  frege91  44663  sbcoreleleq  45227  onfrALTlem4  45235  sbcoreleleqVD  45550  onfrALTlem4VD  45577  rspesbcd  45629