Theorem abbidv 2354

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)

Hypothesis

Ref	Expression
abbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
abbidv	⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 ⊢ Ⅎ𝑥𝜑
2		abbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	abbid 2351	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  {cab 2220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227

This theorem is referenced by:  rabbidva2  2799  cdeqab  3035  sbceqbid  3052  csbeq1  3144  sbcel12g  3156  sbceqg  3157  csbeq2  3165  csbeq2d  3166  csbnestgf  3194  csbprc  3558  ifbi  3647  pweq  3677  sneq  3705  csbsng  3755  rabsn  3761  dfopg  3886  opeq1  3888  opeq2  3889  csbunig  3927  unieq  3928  inteq  3957  iineq1  4010  iineq2  4013  dfiin2g  4029  iinrabm  4059  iinxprg  4071  opabbid  4180  dcextest  4708  csbxpg  4836  csbdmg  4955  imasng  5132  csbrng  5229  iotaeq  5326  iotabi  5327  dfimafn  5730  fnsnfv  5741  fndmin  5790  dfimafnf  5928  fliftf  5978  oprabbid  6114  recseq  6550  freceq1  6636  freceq2  6637  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  qseq1  6830  qseq2  6831  qsinxp  6858  mapvalg  6905  ixpsnval  6949  ixpeq1  6957  snexxph  7233  fival  7270  acneq  7522  prplnqu  7951  cauappcvgprlemlim  7992  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgsr  8133  pitonnlem2  8178  pitonn  8179  recidpipr  8187  nntopi  8225  axcaucvglemval  8228  csbwrdg  11279  shftlem  11526  shftfibg  11530  shftdm  11532  shftfib  11533  negfi  11938  tgval  13559  ptex  13561  eqglact  14026  isghm  14044  ixpsnbasval  14726  plyval  15709  vtxdfifiun  16404