Theorem abbidv 2257

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331  {cab 2125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132

This theorem is referenced by:  rabbidva2  2673  cdeqab  2899  csbeq1  3006  sbcel12g  3017  sbceqg  3018  csbeq2  3026  csbeq2d  3027  csbnestgf  3052  csbprc  3408  ifbi  3492  pweq  3513  sneq  3538  csbsng  3584  rabsn  3590  dfopg  3703  opeq1  3705  opeq2  3706  csbunig  3744  unieq  3745  inteq  3774  iineq1  3827  iineq2  3830  dfiin2g  3846  iinrabm  3875  iinxprg  3887  opabbid  3993  dcextest  4495  csbxpg  4620  csbdmg  4733  imasng  4904  csbrng  5000  iotaeq  5096  iotabi  5097  dfimafn  5470  fnsnfv  5480  fndmin  5527  fliftf  5700  oprabbid  5824  recseq  6203  freceq1  6289  freceq2  6290  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  qseq1  6477  qseq2  6478  qsinxp  6505  mapvalg  6552  ixpsnval  6595  ixpeq1  6603  snexxph  6838  fival  6858  prplnqu  7428  cauappcvgprlemlim  7469  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnkeqj  7498  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexbt  7514  caucvgprprlem1  7517  caucvgprprlem2  7518  caucvgsr  7610  pitonnlem2  7655  pitonn  7656  recidpipr  7664  nntopi  7702  axcaucvglemval  7705  shftlem  10588  shftfibg  10592  shftdm  10594  shftfib  10595  negfi  10999  tgval  12218