Theorem abbidv 2232

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1314  {cab 2101

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108

This theorem is referenced by:  rabbidva2  2644  cdeqab  2868  csbeq1  2974  sbcel12g  2984  sbceqg  2985  csbeq2d  2993  csbnestgf  3018  csbprc  3374  ifbi  3458  pweq  3479  sneq  3504  csbsng  3550  rabsn  3556  dfopg  3669  opeq1  3671  opeq2  3672  csbunig  3710  unieq  3711  inteq  3740  iineq1  3793  iineq2  3796  dfiin2g  3812  iinrabm  3841  iinxprg  3853  opabbid  3953  dcextest  4455  csbxpg  4580  csbdmg  4693  imasng  4862  csbrng  4958  iotaeq  5054  iotabi  5055  dfimafn  5424  fnsnfv  5434  fndmin  5481  fliftf  5654  oprabbid  5778  recseq  6157  freceq1  6243  freceq2  6244  frec0g  6248  freccllem  6253  frecfcllem  6255  frecsuclem  6257  frecsuc  6258  qseq1  6431  qseq2  6432  qsinxp  6459  mapvalg  6506  ixpsnval  6549  ixpeq1  6557  snexxph  6790  fival  6810  prplnqu  7376  cauappcvgprlemlim  7417  caucvgprprlemell  7441  caucvgprprlemelu  7442  caucvgprprlemcbv  7443  caucvgprprlemval  7444  caucvgprprlemnkeqj  7446  caucvgprprlemml  7450  caucvgprprlemmu  7451  caucvgprprlemopl  7453  caucvgprprlemlol  7454  caucvgprprlemopu  7455  caucvgprprlemloc  7459  caucvgprprlemclphr  7461  caucvgprprlemexbt  7462  caucvgprprlem1  7465  caucvgprprlem2  7466  caucvgsr  7544  pitonnlem2  7582  pitonn  7583  recidpipr  7591  nntopi  7629  axcaucvglemval  7632  shftlem  10481  shftfibg  10485  shftdm  10487  shftfib  10488  negfi  10891  tgval  12061