Theorem abbidv 2327

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 1554	. 2 ⊢ Ⅎ𝑥𝜑
2		abbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	abbid 2326	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375  {cab 2195

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202

This theorem is referenced by:  rabbidva2  2766  cdeqab  2998  sbceqbid  3015  csbeq1  3107  sbcel12g  3119  sbceqg  3120  csbeq2  3128  csbeq2d  3129  csbnestgf  3157  csbprc  3517  ifbi  3603  pweq  3632  sneq  3657  csbsng  3707  rabsn  3713  dfopg  3834  opeq1  3836  opeq2  3837  csbunig  3875  unieq  3876  inteq  3905  iineq1  3958  iineq2  3961  dfiin2g  3977  iinrabm  4007  iinxprg  4019  opabbid  4128  dcextest  4650  csbxpg  4777  csbdmg  4894  imasng  5069  csbrng  5166  iotaeq  5263  iotabi  5264  dfimafn  5655  fnsnfv  5666  fndmin  5715  fliftf  5896  oprabbid  6028  recseq  6422  freceq1  6508  freceq2  6509  frec0g  6513  freccllem  6518  frecfcllem  6520  frecsuclem  6522  frecsuc  6523  qseq1  6700  qseq2  6701  qsinxp  6728  mapvalg  6775  ixpsnval  6818  ixpeq1  6826  snexxph  7085  fival  7105  acneq  7352  prplnqu  7775  cauappcvgprlemlim  7816  caucvgprprlemell  7840  caucvgprprlemelu  7841  caucvgprprlemcbv  7842  caucvgprprlemval  7843  caucvgprprlemnkeqj  7845  caucvgprprlemml  7849  caucvgprprlemmu  7850  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemopu  7854  caucvgprprlemloc  7858  caucvgprprlemclphr  7860  caucvgprprlemexbt  7861  caucvgprprlem1  7864  caucvgprprlem2  7865  caucvgsr  7957  pitonnlem2  8002  pitonn  8003  recidpipr  8011  nntopi  8049  axcaucvglemval  8052  csbwrdg  11067  shftlem  11293  shftfibg  11297  shftdm  11299  shftfib  11300  negfi  11705  tgval  13261  ptex  13263  eqglact  13728  isghm  13746  ixpsnbasval  14395  plyval  15371