Theorem rabbidv 3399

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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3398	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {crab 3392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-rab 3393

This theorem is referenced by:  difeq2  4058  seex  5584  mptiniseg  6197  dfpred3g  6271  elovmporab  7609  elovmpt3rab1  7623  naddcllem  8609  naddov2  8612  naddcom  8615  naddrid  8616  naddass  8629  fineqvlem  9173  mapfien2  9319  supeq1  9355  supeq2  9358  supeq3  9359  oieq1  9424  oieq2  9425  ordtypecbv  9429  ordtypelem3  9432  harval  9472  inf3lema  9543  wemapwe  9616  oef1o  9617  tz9.12lem3  9711  rankvalb  9719  rankvalg  9739  ranksnb  9749  rankonidlem  9750  cardval3  9874  cardidm  9881  alephsuc2  10000  coftr  10193  fin1a2lem11  10330  fin1a2lem12  10331  hsmex  10352  axdc3lem2  10371  zorn2lem1  10416  zorn2lem6  10421  zorn2lem7  10422  zorn2g  10423  wuncval  10663  tskmval  10760  peano5uzti  12617  uzval  12788  rpnnen1  12931  ixxval  13304  fzval  13461  hashbclem  14412  hashbc  14413  shftfn  15033  bitsfval  16390  sadfval  16419  sadcom  16430  smufval  16444  smupp1  16447  smupval  16455  smumullem  16459  gcdval  16463  bezoutlem2  16507  bezoutlem4  16509  lcmval  16559  lcmfval  16588  lcmf0val  16589  lcmfpr  16594  isprm  16640  odzval  16760  pcval  16813  pceulem  16814  pceu  16815  pczpre  16816  pcdiv  16821  prmreclem1  16885  prmreclem4  16888  prmreclem5  16889  ramval  16977  cshws0  17070  imasdsval  17477  mrcval  17574  eldmcoa  18030  chneq1  18576  cycsubg2  19183  cntzval  19294  cntzsnval  19297  odfval  19505  odfvalALT  19506  odval  19507  gexval  19551  efgsfo  19712  dprdval  19978  ablfac1a  20044  ablfac1b  20045  ablfac1eu  20048  ablfaclem1  20060  ablfaclem3  20062  rnghmval  20418  rgspnval  20591  lspval  20972  ocvval  21649  dsmmelbas  21721  frlmsslss  21756  aspval  21854  psrass1lem  21915  psrmulval  21926  mplmonmul  22019  mhpval  22134  mhpmulcl  22144  coe1mul2  22262  pmatcoe1fsupp  22691  istopon  22902  toponsspwpw  22912  clsval  23027  neival  23092  ordtbaslem  23178  ordtbas2  23181  ordtopn1  23184  ordtopn2  23185  cnpval  23226  llyeq  23460  nllyeq  23461  ptfinfin  23509  finlocfin  23510  dissnlocfin  23519  locfindis  23520  xkoopn  23579  kqfval  23713  tsmsfbas  24118  blvalps  24375  blval  24376  nmofval  24704  nmoval  24705  ishtpy  24964  minveclem3b  25420  minveclem3  25421  minveclem4  25424  minveclem5  25425  ovolval  25465  vitalilem2  25601  vitalilem3  25602  vitalilem4  25603  vitali  25605  itg2monolem1  25742  elcpn  25926  mdegmullem  26068  elqaalem1  26310  elqaalem2  26311  elqaalem3  26312  elqaa  26313  aannenlem1  26319  aannenlem2  26320  jensen  26977  vmaval  27101  muval  27120  sgmval  27130  fsumdvdscom  27173  musum  27179  muinv  27181  dchrisum0fval  27493  dchrisum0ff  27495  logsqvma2  27531  pntrlog2bndlem1  27565  cutsval  27797  bdayons  28293  tglngval  28644  ttgval  28968  ttgitvval  28975  ebtwntg  29076  numedglnl  29238  dfnbgr2  29431  dfnbgr3  29432  uvtxusgr  29496  vtxdgval  29562  rusgrnumwrdl2  29680  iswwlksnon  29946  rusgrnumwwlks  30070  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  clwlknf1oclwwlknlem2  30177  clwwlknon  30185  clwwlk0on0  30187  eupth2  30334  fusgreg2wsplem  30428  fusgreghash2wsp  30433  numclwlk1lem1  30464  sspval  30819  ubthlem1  30966  ubthlem2  30967  ubthlem3  30968  ocval  31376  spanval  31429  chsupid  31508  eigvecval  31992  specval  31994  iunpreima  32660  fcobijfs2  32821  pwrssmgc  33086  fxpgaval  33255  nsgqusf1olem3  33505  selvply1rhmlemb  33710  mplvrpmrhm  33738  psrmonmul  33741  esplyfval  33754  esplyfval0  33755  minplyval  33896  constrsuc  33929  constrcbvlem  33946  crefeq  34036  zarcls1  34060  zarclsun  34061  zarclsiin  34062  zarclsint  34063  zarclssn  34064  zartop  34067  zartopon  34068  zart0  34070  zarmxt1  34071  zarcmp  34073  rhmpreimacnlem  34075  rhmpreimacn  34076  ordtcnvNEW  34111  ordtrest2NEW  34114  ordtconnlem1  34115  measvuni  34405  brfae  34439  omsfval  34485  orvcelval  34660  ballotlemi  34692  bnj602  35104  fineqvnttrclselem2  35310  fineqvnttrclselem3  35311  fineqvnttrclse  35312  onvf1odlem3  35340  subfacp1lem6  35420  kur14  35451  cvmscbv  35493  cvmsi  35500  cvmsval  35501  snmlval  35566  snmlflim  35567  satfv0  35593  satfv1  35598  satfv0fun  35606  satffunlem1lem1  35637  satffunlem2lem1  35639  satfv0fvfmla0  35648  satfv1fvfmla1  35658  prv1n  35666  fvray  36376  fwddifnval  36398  neibastop3  36597  weiunlem  36698  icoreval  37722  fin2so  37981  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  poimirlem32  38026  ftc1anclem6  38072  islinei  40239  pmapval  40256  paddval  40297  paddcom  40312  pclvalN  40389  ldilset  40608  dilsetN  40652  diafval  41530  diaval  41531  docavalN  41622  dicfval  41674  dochfval  41849  dochval  41850  mapdval  42127  mapdsn2  42141  grpods  42686  unitscyglem1  42687  unitscyglem2  42688  unitscyglem3  42689  unitscyglem4  42690  prjcrvval  43089  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  eldioph4i  43264  diophren  43265  pell1qrval  43298  pell14qrval  43300  pell1234qrval  43302  rpnnen3  43484  fnwe2lem1  43502  pwssplit4  43541  pwslnmlem2  43545  dgraaval  43596  itgoval  43613  proot1hash  43647  rp-intrabeq  43673  rp-unirabeq  43674  rfovfvd  44453  rfovfvfvd  44454  rfovcnvf1od  44455  fsovrfovd  44460  fsovfvd  44461  fsovfvfvd  44462  fsovcnvlem  44464  nzss  44768  supminfxr  45914  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  dvnprod  46399  stoweidlem26  46476  stoweidlem27  46477  stoweidlem31  46481  stoweidlem34  46484  stoweidlem46  46496  fourierdlem79  46635  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem105  46661  fourierdlem107  46663  fourierdlem108  46664  fourierdlem110  46666  etransclem11  46695  salgenval  46771  subsaliuncl  46808  ovnval  46991  ovnval2  46995  ovnval2b  47002  ovncvrrp  47014  ovnsubaddlem1  47020  ovnsubadd  47022  ovncvr2  47061  hspmbl  47079  ovolval2  47094  ovnovollem3  47108  salpreimagelt  47157  salpreimalegt  47159  salpreimagtge  47175  salpreimaltle  47176  issmflem  47177  issmf  47178  salpreimagtlt  47180  smfpreimalt  47181  smfpreimaltf  47186  issmfle  47195  smfpimltxr  47197  smfpreimale  47204  issmfgt  47206  smfpreimagt  47212  issmfge  47220  smflimlem3  47223  smflimlem4  47224  smflim  47227  smfpimgtxr  47230  smfpreimage  47232  fvmptrabdm  47763  elsetpreimafveq  47879  prmdvdsfmtnof1  48072  fppr  48224  dfclnbgr2  48321  dfclnbgr3  48324  dfsclnbgr6  48356  grlimedgclnbgr  48493  grlimgrtri  48501  grilcbri2  48509  bigoval  49047  line  49230  rrxline  49232  sphere  49245  line2y  49253  inpw  49322