Theorem abbidv 2352

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 2349	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

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

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 2214

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

This theorem is referenced by:  rabbidva2  2796  cdeqab  3031  sbceqbid  3048  csbeq1  3140  sbcel12g  3152  sbceqg  3153  csbeq2  3161  csbeq2d  3162  csbnestgf  3190  csbprc  3553  ifbi  3642  pweq  3671  sneq  3699  csbsng  3749  rabsn  3755  dfopg  3880  opeq1  3882  opeq2  3883  csbunig  3921  unieq  3922  inteq  3951  iineq1  4004  iineq2  4007  dfiin2g  4023  iinrabm  4053  iinxprg  4065  opabbid  4174  dcextest  4702  csbxpg  4830  csbdmg  4949  imasng  5126  csbrng  5223  iotaeq  5320  iotabi  5321  dfimafn  5724  fnsnfv  5735  fndmin  5784  fliftf  5971  oprabbid  6105  recseq  6536  freceq1  6622  freceq2  6623  frec0g  6627  freccllem  6632  frecfcllem  6634  frecsuclem  6636  frecsuc  6637  qseq1  6816  qseq2  6817  qsinxp  6844  mapvalg  6891  ixpsnval  6935  ixpeq1  6943  snexxph  7219  fival  7256  acneq  7508  prplnqu  7934  cauappcvgprlemlim  7975  caucvgprprlemell  7999  caucvgprprlemelu  8000  caucvgprprlemcbv  8001  caucvgprprlemval  8002  caucvgprprlemnkeqj  8004  caucvgprprlemml  8008  caucvgprprlemmu  8009  caucvgprprlemopl  8011  caucvgprprlemlol  8012  caucvgprprlemopu  8013  caucvgprprlemloc  8017  caucvgprprlemclphr  8019  caucvgprprlemexbt  8020  caucvgprprlem1  8023  caucvgprprlem2  8024  caucvgsr  8116  pitonnlem2  8161  pitonn  8162  recidpipr  8170  nntopi  8208  axcaucvglemval  8211  csbwrdg  11250  shftlem  11497  shftfibg  11501  shftdm  11503  shftfib  11504  negfi  11909  tgval  13467  ptex  13469  eqglact  13934  isghm  13952  ixpsnbasval  14606  plyval  15589  vtxdfifiun  16284