Theorem sbcbii 3836

Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.)

Hypothesis

Ref	Expression
sbcbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem sbcbii

Step	Hyp	Ref	Expression
1		sbcbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	sbcbidv 3835	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	mptru 1541	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Syntax hints:   ↔ wb 205  ⊤wtru 1535  [wsbc 3775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-sbc 3776

This theorem is referenced by:  eqsbc2  3844  sbc3an  3845  sbccomlem  3862  sbccom  3863  sbcrext  3865  sbcabel  3870  csbcow  3906  csbco  3907  sbcnel12g  4408  sbcne12  4409  csbcom  4414  csbnestgfw  4416  csbnestgf  4421  sbccsb  4430  sbccsb2  4431  csbab  4434  2nreu  4438  sbcssg  4518  sbcop  5485  sbcrel  5776  difopabOLD  5827  sbcfung  6572  tfinds2  7863  frpoins3xpg  8143  frpoins3xp3g  8144  mpoxopovel  8224  f1od2  32632  bnj62  34575  bnj89  34576  bnj156  34583  bnj524  34592  bnj610  34602  bnj919  34622  bnj976  34632  bnj110  34713  bnj91  34716  bnj92  34717  bnj106  34723  bnj121  34725  bnj124  34726  bnj125  34727  bnj126  34728  bnj130  34729  bnj154  34733  bnj155  34734  bnj153  34735  bnj207  34736  bnj523  34742  bnj526  34743  bnj539  34746  bnj540  34747  bnj581  34763  bnj591  34766  bnj609  34772  bnj611  34773  bnj934  34790  bnj1000  34796  bnj984  34807  bnj985v  34808  bnj985  34809  bnj1040  34827  bnj1123  34841  bnj1452  34907  bnj1463  34910  sbcalf  37825  sbcexf  37826  sbccom2lem  37835  sbccom2  37836  sbccom2f  37837  sbccom2fi  37838  csbcom2fi  37839  rspcsbnea  41840  2sbcrex  42475  2sbcrexOLD  42477  sbcrot3  42482  sbcrot5  42483  2rexfrabdioph  42487  3rexfrabdioph  42488  4rexfrabdioph  42489  6rexfrabdioph  42490  7rexfrabdioph  42491  rmydioph  42706  expdiophlem2  42714  sbcheg  43480  sbc3or  44242  trsbc  44250  onfrALTlem5  44252  eqsbc2VD  44550  sbcoreleleqVD  44569  onfrALTlem5VD  44595  ich2exprop  47076