Theorem abbidv 2728

Description: Equivalent wff's yield equal class abstractions (deduction rule). (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 1830	. 2 ⊢ Ⅎ𝑥𝜑
2		abbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	abbid 2727	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606

This theorem is referenced by:  rabbidva2  3162  cdeqab  3392  sbceqbid  3409  csbeq1  3502  csbeq2  3503  csbprc  3932  csbprcOLD  3933  sbcel12  3935  sbceqg  3936  csbeq2d  3943  csbnestgf  3948  pweq  4111  sneq  4135  csbsng  4190  rabsn  4200  unieq  4380  csbuni  4402  inteq  4413  iineq1  4471  iineq2  4474  dfiin2g  4489  iinrab  4518  iinxprg  4537  opabbid  4647  imasng  5406  iotaeq  5776  iotabi  5777  dfimafn  6155  fnsnfv  6168  fliftf  6465  oprabbid  6606  wrecseq123  7295  rdglim2  7415  qseq1  7683  qseq2  7684  qsinxp  7710  mapvalg  7754  ixpsnval  7797  ixpeq1  7805  fival  8201  tcvalg  8497  karden  8641  acneq  8749  infmap2  8923  cfval  8952  cflim3  8967  axdclem  9224  axdc  9226  rankcf  9478  genpv  9700  negfi  10850  supadd  10868  hashf1lem2  13097  hashf1  13098  hashfac  13099  csbwrdg  13189  cshimadifsn  13426  cshimadifsn0  13427  cleq1  13570  dfrtrcl2  13650  shftlem  13656  shftfib  13660  vdwlem6  15528  cshwsiun  15644  lubfval  16801  glbfval  16814  eqglact  17468  isghm  17483  symgval  17622  sylow1lem2  17837  sylow3lem1  17865  efgval  17953  dmdprd  18220  ixpsnbasval  19030  aspval2  19168  ressmplbas2  19276  cssval  19845  tgval  20570  clsval2  20664  lpfval  20752  lpval  20753  islocfin  21130  ptval  21183  hauspwpwf1  21601  ptcmplem2  21667  snclseqg  21729  ustval  21816  itg2val  23301  limcfval  23442  plyval  23753  isismt  25229  nbgraf1olem5  25974  nb3graprlem1  25980  fargshiftfo  26166  wwlknprop  26214  wwlknfi  26266  eclclwwlkn1  26359  rusgranumwlkb0  26480  rusgra0edg  26482  avril1  26711  nmoofval  27001  nmooval  27002  nmoo0  27030  nmopval  28099  nmfnval  28119  iunrdx  28764  disjabrex  28777  disjabrexf  28778  dfimafnf  28817  curry2ima  28869  pstmval  29266  pstmfval  29267  sigaval  29500  measval  29588  orvcval  29846  bnj956  30101  bnj18eq1  30251  bnj1318  30347  derangval  30403  mclsval  30714  dfrdg2  30945  dfrdg3  30946  altxpeq1  31250  altxpeq2  31251  bj-snsetex  32144  bj-sngleq  32148  bj-projeq  32173  bj-projval  32177  csbwrecsg  32349  csboprabg  32352  finxpeq1  32399  finxpeq2  32400  csbfinxpg  32401  finxpreclem6  32409  ptrest  32578  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  mblfinlem3  32618  cnambfre  32628  itg2addnc  32634  areacirclem5  32674  sdclem2  32708  sdc  32710  ismtyval  32769  elghomlem1OLD  32854  iineq12f  33143  lfl1dim  33426  ldual1dim  33471  glbconxN  33682  lineset  34042  pointsetN  34045  psubspset  34048  pmapglb2xN  34076  polval2N  34210  psubclsetN  34240  lautset  34386  pautsetN  34402  tendofset  35064  tendoset  35065  dva1dim  35291  dia1dim2  35369  dib1dim2  35475  diclspsn  35501  dih1dimatlem  35636  dihglb2  35649  hdmap1ffval  36103  hdmapffval  36136  hgmapffval  36195  eldiophb  36338  eldioph  36339  diophrw  36340  eldioph2  36343  eldioph2b  36344  eldioph3  36347  diophin  36354  diophun  36355  diophrex  36357  rexrabdioph  36376  rmxypairf1o  36494  hbtlem1  36712  hbtlem7  36714  nzss  37538  dropab1  37672  dropab2  37673  sbcel12gOLD  37775  csbunigOLD  38073  csbfv12gALTOLD  38074  csbxpgOLD  38075  csbrngOLD  38078  supsubc  38510  dfaimafn  39894  rnfdmpr  40325  nb3grprlem1  40608  vtxdun  40696  rgrx0ndm  40793  ewlksfval  40803  wwlksnfi  41112  rusgrnumwwlkb0  41174  eclclwwlksn1  41259  setrecseq  42231