Theorem rabbidv 3408

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 3407	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3402

This theorem is referenced by:  difeq2  4074  seex  5591  mptiniseg  6205  dfpred3g  6279  elovmporab  7614  elovmpt3rab1  7628  naddcllem  8614  naddov2  8617  naddcom  8620  naddrid  8621  naddass  8634  fineqvlem  9178  mapfien2  9324  supeq1  9360  supeq2  9363  supeq3  9364  oieq1  9429  oieq2  9430  ordtypecbv  9434  ordtypelem3  9437  harval  9477  inf3lema  9545  wemapwe  9618  oef1o  9619  tz9.12lem3  9713  rankvalb  9721  rankvalg  9741  ranksnb  9751  rankonidlem  9752  cardval3  9876  cardidm  9883  alephsuc2  10002  coftr  10195  fin1a2lem11  10332  fin1a2lem12  10333  hsmex  10354  axdc3lem2  10373  zorn2lem1  10418  zorn2lem6  10423  zorn2lem7  10424  zorn2g  10425  wuncval  10665  tskmval  10762  peano5uzti  12594  uzval  12765  rpnnen1  12908  ixxval  13281  fzval  13437  hashbclem  14387  hashbc  14388  shftfn  15008  bitsfval  16362  sadfval  16391  sadcom  16402  smufval  16416  smupp1  16419  smupval  16427  smumullem  16431  gcdval  16435  bezoutlem2  16479  bezoutlem4  16481  lcmval  16531  lcmfval  16560  lcmf0val  16561  lcmfpr  16566  isprm  16612  odzval  16731  pcval  16784  pceulem  16785  pceu  16786  pczpre  16787  pcdiv  16792  prmreclem1  16856  prmreclem4  16859  prmreclem5  16860  ramval  16948  cshws0  17041  imasdsval  17448  mrcval  17545  eldmcoa  18001  chneq1  18547  cycsubg2  19151  cntzval  19262  cntzsnval  19265  odfval  19473  odfvalALT  19474  odval  19475  gexval  19519  efgsfo  19680  dprdval  19946  ablfac1a  20012  ablfac1b  20013  ablfac1eu  20016  ablfaclem1  20028  ablfaclem3  20030  rnghmval  20388  rgspnval  20557  lspval  20938  ocvval  21634  dsmmelbas  21706  frlmsslss  21741  aspval  21840  psrass1lem  21900  psrmulval  21912  mplmonmul  22003  mhpval  22094  mhpmulcl  22104  coe1mul2  22223  pmatcoe1fsupp  22657  istopon  22868  toponsspwpw  22878  clsval  22993  neival  23058  ordtbaslem  23144  ordtbas2  23147  ordtopn1  23150  ordtopn2  23151  cnpval  23192  llyeq  23426  nllyeq  23427  ptfinfin  23475  finlocfin  23476  dissnlocfin  23485  locfindis  23486  xkoopn  23545  kqfval  23679  tsmsfbas  24084  blvalps  24341  blval  24342  nmofval  24670  nmoval  24671  ishtpy  24939  minveclem3b  25396  minveclem3  25397  minveclem4  25400  minveclem5  25401  ovolval  25442  vitalilem2  25578  vitalilem3  25579  vitalilem4  25580  vitali  25582  itg2monolem1  25719  elcpn  25904  mdegmullem  26051  elqaalem1  26295  elqaalem2  26296  elqaalem3  26297  elqaa  26298  aannenlem1  26304  aannenlem2  26305  jensen  26967  vmaval  27091  muval  27110  sgmval  27120  fsumdvdscom  27163  musum  27169  muinv  27171  dchrisum0fval  27484  dchrisum0ff  27486  logsqvma2  27522  pntrlog2bndlem1  27556  cutsval  27788  bdayons  28284  tglngval  28635  ttgval  28959  ttgitvval  28966  ebtwntg  29067  numedglnl  29229  dfnbgr2  29422  dfnbgr3  29423  uvtxusgr  29487  vtxdgval  29554  rusgrnumwrdl2  29672  iswwlksnon  29938  rusgrnumwwlks  30062  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwlknf1oclwwlknlem2  30169  clwwlknon  30177  clwwlk0on0  30179  eupth2  30326  fusgreg2wsplem  30420  fusgreghash2wsp  30425  numclwlk1lem1  30456  sspval  30810  ubthlem1  30957  ubthlem2  30958  ubthlem3  30959  ocval  31367  spanval  31420  chsupid  31499  eigvecval  31983  specval  31985  iunpreima  32650  fcobijfs2  32811  pwrssmgc  33092  fxpgaval  33260  nsgqusf1olem3  33507  mplvrpmrhm  33723  psrmonmul  33726  esplyfval  33739  esplyfval0  33740  minplyval  33882  constrsuc  33915  constrcbvlem  33932  crefeq  34022  zarcls1  34046  zarclsun  34047  zarclsiin  34048  zarclsint  34049  zarclssn  34050  zartop  34053  zartopon  34054  zart0  34056  zarmxt1  34057  zarcmp  34059  rhmpreimacnlem  34061  rhmpreimacn  34062  ordtcnvNEW  34097  ordtrest2NEW  34100  ordtconnlem1  34101  measvuni  34391  brfae  34425  omsfval  34471  orvcelval  34646  ballotlemi  34678  bnj602  35090  fineqvnttrclselem2  35297  fineqvnttrclselem3  35298  fineqvnttrclse  35299  onvf1odlem3  35318  subfacp1lem6  35398  kur14  35429  cvmscbv  35471  cvmsi  35478  cvmsval  35479  snmlval  35544  snmlflim  35545  satfv0  35571  satfv1  35576  satfv0fun  35584  satffunlem1lem1  35615  satffunlem2lem1  35617  satfv0fvfmla0  35626  satfv1fvfmla1  35636  prv1n  35644  fvray  36354  fwddifnval  36376  neibastop3  36575  weiunlem  36676  icoreval  37602  fin2so  37852  poimirlem26  37891  poimirlem27  37892  poimirlem28  37893  poimirlem32  37897  ftc1anclem6  37943  islinei  40110  pmapval  40127  paddval  40168  paddcom  40183  pclvalN  40260  ldilset  40479  dilsetN  40523  diafval  41401  diaval  41402  docavalN  41493  dicfval  41545  dochfval  41720  dochval  41721  mapdval  41998  mapdsn2  42012  grpods  42558  unitscyglem1  42559  unitscyglem2  42560  unitscyglem3  42561  unitscyglem4  42562  prjcrvval  42984  2rexfrabdioph  43147  3rexfrabdioph  43148  4rexfrabdioph  43149  6rexfrabdioph  43150  7rexfrabdioph  43151  eldioph4i  43163  diophren  43164  pell1qrval  43197  pell14qrval  43199  pell1234qrval  43201  rpnnen3  43383  fnwe2lem1  43401  pwssplit4  43440  pwslnmlem2  43444  dgraaval  43495  itgoval  43512  proot1hash  43546  rp-intrabeq  43572  rp-unirabeq  43573  rfovfvd  44352  rfovfvfvd  44353  rfovcnvf1od  44354  fsovrfovd  44359  fsovfvd  44360  fsovfvfvd  44361  fsovcnvlem  44363  nzss  44667  supminfxr  45816  dvnprodlem1  46298  dvnprodlem2  46299  dvnprodlem3  46300  dvnprod  46301  stoweidlem26  46378  stoweidlem27  46379  stoweidlem31  46383  stoweidlem34  46386  stoweidlem46  46398  fourierdlem79  46537  fourierdlem96  46554  fourierdlem97  46555  fourierdlem98  46556  fourierdlem99  46557  fourierdlem105  46563  fourierdlem107  46565  fourierdlem108  46566  fourierdlem110  46568  etransclem11  46597  salgenval  46673  subsaliuncl  46710  ovnval  46893  ovnval2  46897  ovnval2b  46904  ovncvrrp  46916  ovnsubaddlem1  46922  ovnsubadd  46924  ovncvr2  46963  hspmbl  46981  ovolval2  46996  ovnovollem3  47010  salpreimagelt  47059  salpreimalegt  47061  salpreimagtge  47077  salpreimaltle  47078  issmflem  47079  issmf  47080  salpreimagtlt  47082  smfpreimalt  47083  smfpreimaltf  47088  issmfle  47097  smfpimltxr  47099  smfpreimale  47106  issmfgt  47108  smfpreimagt  47114  issmfge  47122  smflimlem3  47125  smflimlem4  47126  smflim  47129  smfpimgtxr  47132  smfpreimage  47134  fvmptrabdm  47647  elsetpreimafveq  47751  prmdvdsfmtnof1  47941  fppr  48080  dfclnbgr2  48177  dfclnbgr3  48180  dfsclnbgr6  48212  grlimedgclnbgr  48349  grlimgrtri  48357  grilcbri2  48365  bigoval  48903  line  49086  rrxline  49088  sphere  49101  line2y  49109  inpw  49178