Theorem abbidv 2324

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  {cab 2192

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199

This theorem is referenced by:  rabbidva2  2760  cdeqab  2989  sbceqbid  3006  csbeq1  3097  sbcel12g  3109  sbceqg  3110  csbeq2  3118  csbeq2d  3119  csbnestgf  3147  csbprc  3507  ifbi  3592  pweq  3620  sneq  3645  csbsng  3695  rabsn  3701  dfopg  3819  opeq1  3821  opeq2  3822  csbunig  3860  unieq  3861  inteq  3890  iineq1  3943  iineq2  3946  dfiin2g  3962  iinrabm  3992  iinxprg  4004  opabbid  4113  dcextest  4633  csbxpg  4760  csbdmg  4877  imasng  5052  csbrng  5149  iotaeq  5245  iotabi  5246  dfimafn  5634  fnsnfv  5645  fndmin  5694  fliftf  5875  oprabbid  6005  recseq  6399  freceq1  6485  freceq2  6486  frec0g  6490  freccllem  6495  frecfcllem  6497  frecsuclem  6499  frecsuc  6500  qseq1  6677  qseq2  6678  qsinxp  6705  mapvalg  6752  ixpsnval  6795  ixpeq1  6803  snexxph  7059  fival  7079  acneq  7321  prplnqu  7740  cauappcvgprlemlim  7781  caucvgprprlemell  7805  caucvgprprlemelu  7806  caucvgprprlemcbv  7807  caucvgprprlemval  7808  caucvgprprlemnkeqj  7810  caucvgprprlemml  7814  caucvgprprlemmu  7815  caucvgprprlemopl  7817  caucvgprprlemlol  7818  caucvgprprlemopu  7819  caucvgprprlemloc  7823  caucvgprprlemclphr  7825  caucvgprprlemexbt  7826  caucvgprprlem1  7829  caucvgprprlem2  7830  caucvgsr  7922  pitonnlem2  7967  pitonn  7968  recidpipr  7976  nntopi  8014  axcaucvglemval  8017  csbwrdg  11030  shftlem  11171  shftfibg  11175  shftdm  11177  shftfib  11178  negfi  11583  tgval  13138  ptex  13140  eqglact  13605  isghm  13623  ixpsnbasval  14272  plyval  15248