Theorem abbidv 2347

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  {cab 2215

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222

This theorem is referenced by:  rabbidva2  2784  cdeqab  3019  sbceqbid  3036  csbeq1  3128  sbcel12g  3140  sbceqg  3141  csbeq2  3149  csbeq2d  3150  csbnestgf  3178  csbprc  3538  ifbi  3624  pweq  3653  sneq  3678  csbsng  3728  rabsn  3734  dfopg  3858  opeq1  3860  opeq2  3861  csbunig  3899  unieq  3900  inteq  3929  iineq1  3982  iineq2  3985  dfiin2g  4001  iinrabm  4031  iinxprg  4043  opabbid  4152  dcextest  4677  csbxpg  4805  csbdmg  4923  imasng  5099  csbrng  5196  iotaeq  5293  iotabi  5294  dfimafn  5690  fnsnfv  5701  fndmin  5750  fliftf  5935  oprabbid  6069  recseq  6467  freceq1  6553  freceq2  6554  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  qseq1  6747  qseq2  6748  qsinxp  6775  mapvalg  6822  ixpsnval  6865  ixpeq1  6873  snexxph  7143  fival  7163  acneq  7410  prplnqu  7833  cauappcvgprlemlim  7874  caucvgprprlemell  7898  caucvgprprlemelu  7899  caucvgprprlemcbv  7900  caucvgprprlemval  7901  caucvgprprlemnkeqj  7903  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemloc  7916  caucvgprprlemclphr  7918  caucvgprprlemexbt  7919  caucvgprprlem1  7922  caucvgprprlem2  7923  caucvgsr  8015  pitonnlem2  8060  pitonn  8061  recidpipr  8069  nntopi  8107  axcaucvglemval  8110  csbwrdg  11136  shftlem  11370  shftfibg  11374  shftdm  11376  shftfib  11377  negfi  11782  tgval  13338  ptex  13340  eqglact  13805  isghm  13823  ixpsnbasval  14473  plyval  15449  vtxdfifiun  16108