Theorem sbcie 3771

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)

Hypotheses

Ref	Expression
sbcie.1	⊢ 𝐴 ∈ V
sbcie.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbcie	⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem sbcie

Step	Hyp	Ref	Expression
1		sbcie.1	. 2 ⊢ 𝐴 ∈ V
2		sbcie.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	sbcieg 3769	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3430  [wsbc 3729

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  sbc2ie  3805  csbie  3873  rexopabb  5476  reuop  6251  tfinds2  7808  soseq  8102  findcard2  9092  ac6sfi  9187  ac6num  10392  fpwwe  10560  nn1suc  12187  wrdind  14675  cjth  15056  fprodser  15905  prmind2  16645  joinlem  18338  meetlem  18352  mndind  18787  isghm  19181  isghmOLD  19182  islmod  20850  islindf  21802  fgcl  23853  cfinfil  23868  csdfil  23869  supfil  23870  fin1aufil  23907  quotval  26269  dfconngr1  30273  isconngr  30274  isconngr1  30275  wrdt2ind  33028  bnj62  34879  bnj610  34906  bnj976  34936  bnj106  35026  bnj125  35030  bnj154  35036  bnj155  35037  bnj526  35046  bnj540  35050  bnj591  35069  bnj609  35075  bnj893  35086  bnj1417  35199  poimirlem27  37982  sdclem2  38077  fdc  38080  fdc1  38081  lshpkrlem3  39572  hdmap1fval  42256  hdmapfval  42287  sn-isghm  43120  rabren3dioph  43261  2nn0ind  43391  zindbi  43392  onfrALTlem5  44987  onfrALTlem5VD  45329  reupr  47994