Theorem sbcbii 3803

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 3802	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	mptru 1577	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571  [wsbc 3747

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-sbc 3748

This theorem is used by:  eqsbc2  3810  sbc3an  3811  sbccomlemOLD  3826  sbccom  3827  sbcrext  3829  sbcabel  3834  csbcow  3871  csbco  3872  sbcnel12g  4382  sbcne12  4383  csbcom  4388  csbnestgfw  4390  csbnestgf  4395  sbccsb  4404  sbccsb2  4405  csbab  4408  2nreu  4412  sbcssg  4487  sbcop  5476  sbcrel  5772  sbcfung  6567  tfinds2  7869  frpoins3xpg  8145  frpoins3xp3g  8146  mpoxopovel  8225  f1od2  33101  bnj62  35141  bnj89  35142  bnj156  35149  bnj524  35158  bnj610  35168  bnj919  35188  bnj976  35198  bnj110  35278  bnj91  35281  bnj92  35282  bnj106  35288  bnj121  35290  bnj124  35291  bnj125  35292  bnj126  35293  bnj130  35294  bnj154  35298  bnj155  35299  bnj153  35300  bnj207  35301  bnj523  35307  bnj526  35308  bnj539  35311  bnj540  35312  bnj581  35328  bnj591  35331  bnj609  35337  bnj611  35338  bnj934  35355  bnj1000  35361  bnj984  35372  bnj985v  35373  bnj985  35374  bnj1040  35392  bnj1123  35406  bnj1452  35472  bnj1463  35475  sbcalf  38804  sbcexf  38805  sbccom2lem  38814  sbccom2  38815  sbccom2f  38816  sbccom2fi  38817  csbcom2fi  38818  rspcsbnea  42939  2sbcrex  43556  sbcrot3  43559  sbcrot5  43560  2rexfrabdioph  43564  3rexfrabdioph  43565  4rexfrabdioph  43566  6rexfrabdioph  43567  7rexfrabdioph  43568  rmydioph  43782  expdiophlem2  43790  sbcheg  44546  sbc3or  45282  trsbc  45290  onfrALTlem5  45292  eqsbc2VD  45589  sbcoreleleqVD  45608  onfrALTlem5VD  45634  ich2exprop  48261