Theorem sbcieg 3817

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2137, ax-12 2171. (Revised by Gino Giotto, 12-Oct-2024.)

Hypothesis

Ref	Expression
sbcieg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbcieg	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem sbcieg

Step	Hyp	Ref	Expression
1		df-sbc 3778	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		sbcieg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	elabg 3666	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	1, 3	bitrid 282	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2709  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778

This theorem is referenced by:  sbcie  3820  2nreu  4441  reuprg0  4706  rabsnif  4727  ralrnmptw  7095  ralrnmpt  7097  fpwwe2lem3  10630  nn1suc  12238  opfi1uzind  14466  mndind  18745  fgcl  23602  cfinfil  23617  csdfil  23618  supfil  23619  fin1aufil  23656  ifeqeqx  32029  nn0min  32281  bnj1452  34349  cdlemk35s  40111  cdlemk39s  40113  cdlemk42  40115  2nn0ind  41986  zindbi  41987  prproropreud  46476