Theorem rabbidv 3440

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)

Hypothesis

Ref	Expression
rabbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3439	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-rab 3433

This theorem is referenced by:  difeq2  4129  seex  5647  mptiniseg  6260  dfpred3g  6334  elovmporab  7678  elovmpt3rab1  7692  naddcllem  8712  naddov2  8715  naddcom  8718  naddrid  8719  naddass  8732  fineqvlem  9295  mapfien2  9446  supeq1  9482  supeq2  9485  supeq3  9486  oieq1  9549  oieq2  9550  ordtypecbv  9554  ordtypelem3  9557  harval  9597  inf3lema  9661  wemapwe  9734  oef1o  9735  tz9.12lem3  9826  rankvalb  9834  rankvalg  9854  ranksnb  9864  rankonidlem  9865  cardval3  9989  cardidm  9996  alephsuc2  10117  coftr  10310  fin1a2lem11  10447  fin1a2lem12  10448  hsmex  10469  axdc3lem2  10488  zorn2lem1  10533  zorn2lem6  10538  zorn2lem7  10539  zorn2g  10540  wuncval  10779  tskmval  10876  peano5uzti  12705  uzval  12877  rpnnen1  13022  ixxval  13391  fzval  13545  hashbclem  14487  hashbc  14488  shftfn  15108  bitsfval  16456  sadfval  16485  sadcom  16496  smufval  16510  smupp1  16513  smupval  16521  smumullem  16525  gcdval  16529  bezoutlem2  16573  bezoutlem4  16575  lcmval  16625  lcmfval  16654  lcmf0val  16655  lcmfpr  16660  isprm  16706  odzval  16824  pcval  16877  pceulem  16878  pceu  16879  pczpre  16880  pcdiv  16885  prmreclem1  16949  prmreclem4  16952  prmreclem5  16953  ramval  17041  cshws0  17135  imasdsval  17561  mrcval  17654  eldmcoa  18118  cycsubg2  19240  cntzval  19351  cntzsnval  19354  odfval  19564  odfvalALT  19565  odval  19566  gexval  19610  efgsfo  19771  dprdval  20037  ablfac1a  20103  ablfac1b  20104  ablfac1eu  20107  ablfaclem1  20119  ablfaclem3  20121  rnghmval  20456  rgspnval  20628  lspval  20990  ocvval  21702  dsmmelbas  21776  frlmsslss  21811  aspval  21910  psrass1lem  21969  psrmulval  21981  mplmonmul  22071  mhpval  22160  mhpmulcl  22170  coe1mul2  22287  pmatcoe1fsupp  22722  istopon  22933  toponsspwpw  22943  clsval  23060  neival  23125  ordtbaslem  23211  ordtbas2  23214  ordtopn1  23217  ordtopn2  23218  cnpval  23259  llyeq  23493  nllyeq  23494  ptfinfin  23542  finlocfin  23543  dissnlocfin  23552  locfindis  23553  xkoopn  23612  kqfval  23746  tsmsfbas  24151  blvalps  24410  blval  24411  nmofval  24750  nmoval  24751  ishtpy  25017  minveclem3b  25475  minveclem3  25476  minveclem4  25479  minveclem5  25480  ovolval  25521  vitalilem2  25657  vitalilem3  25658  vitalilem4  25659  vitali  25661  itg2monolem1  25799  elcpn  25984  mdegmullem  26131  elqaalem1  26375  elqaalem2  26376  elqaalem3  26377  elqaa  26378  aannenlem1  26384  aannenlem2  26385  jensen  27046  vmaval  27170  muval  27189  sgmval  27199  fsumdvdscom  27242  musum  27248  muinv  27250  dchrisum0fval  27563  dchrisum0ff  27565  logsqvma2  27601  pntrlog2bndlem1  27635  scutval  27859  tglngval  28573  ttgval  28897  ttgvalOLD  28898  ttgitvval  28910  ebtwntg  29011  numedglnl  29175  dfnbgr2  29368  dfnbgr3  29369  uvtxusgr  29433  vtxdgval  29500  rusgrnumwrdl2  29618  iswwlksnon  29882  rusgrnumwwlks  30003  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwlknf1oclwwlknlem2  30110  clwwlknon  30118  clwwlk0on0  30120  eupth2  30267  fusgreg2wsplem  30361  fusgreghash2wsp  30366  numclwlk1lem1  30397  sspval  30751  ubthlem1  30898  ubthlem2  30899  ubthlem3  30900  ocval  31308  spanval  31361  chsupid  31440  eigvecval  31924  specval  31926  iunpreima  32584  pwrssmgc  32974  nsgqusf1olem3  33422  minplyval  33712  constrsuc  33742  crefeq  33805  zarcls1  33829  zarclsun  33830  zarclsiin  33831  zarclsint  33832  zarclssn  33833  zartop  33836  zartopon  33837  zart0  33839  zarmxt1  33840  zarcmp  33842  rhmpreimacnlem  33844  rhmpreimacn  33845  ordtcnvNEW  33880  ordtrest2NEW  33883  ordtconnlem1  33884  measvuni  34194  brfae  34228  omsfval  34275  orvcelval  34449  ballotlemi  34481  bnj602  34907  subfacp1lem6  35169  kur14  35200  cvmscbv  35242  cvmsi  35249  cvmsval  35250  snmlval  35315  snmlflim  35316  satfv0  35342  satfv1  35347  satfv0fun  35355  satffunlem1lem1  35386  satffunlem2lem1  35388  satfv0fvfmla0  35397  satfv1fvfmla1  35407  prv1n  35415  fvray  36122  fwddifnval  36144  neibastop3  36344  weiunlem2  36445  icoreval  37335  fin2so  37593  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem32  37638  ftc1anclem6  37684  islinei  39722  pmapval  39739  paddval  39780  paddcom  39795  pclvalN  39872  ldilset  40091  dilsetN  40135  diafval  41013  diaval  41014  docavalN  41105  dicfval  41157  dochfval  41332  dochval  41333  mapdval  41610  mapdsn2  41624  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  prjcrvval  42618  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  eldioph4i  42799  diophren  42800  pell1qrval  42833  pell14qrval  42835  pell1234qrval  42837  rpnnen3  43020  fnwe2lem1  43038  pwssplit4  43077  pwslnmlem2  43081  dgraaval  43132  itgoval  43149  proot1hash  43183  rp-intrabeq  43209  rp-unirabeq  43210  rfovfvd  43991  rfovfvfvd  43992  rfovcnvf1od  43993  fsovrfovd  43998  fsovfvd  43999  fsovfvfvd  44000  fsovcnvlem  44002  nzss  44312  supminfxr  45413  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  dvnprod  45904  stoweidlem26  45981  stoweidlem27  45982  stoweidlem31  45986  stoweidlem34  45989  stoweidlem46  46001  fourierdlem79  46140  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem105  46166  fourierdlem107  46168  fourierdlem108  46169  fourierdlem110  46171  etransclem11  46200  salgenval  46276  subsaliuncl  46313  ovnval  46496  ovnval2  46500  ovnval2b  46507  ovncvrrp  46519  ovnsubaddlem1  46525  ovnsubadd  46527  ovncvr2  46566  hspmbl  46584  ovolval2  46599  ovnovollem3  46613  salpreimagelt  46662  salpreimalegt  46664  salpreimagtge  46680  salpreimaltle  46681  issmflem  46682  issmf  46683  salpreimagtlt  46685  smfpreimalt  46686  smfpreimaltf  46691  issmfle  46700  smfpimltxr  46702  smfpreimale  46709  issmfgt  46711  smfpreimagt  46717  issmfge  46725  smflimlem3  46728  smflimlem4  46729  smflim  46732  smfpimgtxr  46735  smfpreimage  46737  fvmptrabdm  47242  elsetpreimafveq  47321  prmdvdsfmtnof1  47511  fppr  47650  dfclnbgr2  47747  dfclnbgr3  47750  dfsclnbgr6  47781  grlimgrtri  47898  grilcbri2  47906  bigoval  48398  line  48581  rrxline  48583  sphere  48596  line2y  48604  inpw  48666