Theorem rabbidv 3397

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

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

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 3391

This theorem is referenced by:  difeq2  4061  seex  5583  mptiniseg  6197  dfpred3g  6271  elovmporab  7606  elovmpt3rab1  7620  naddcllem  8605  naddov2  8608  naddcom  8611  naddrid  8612  naddass  8625  fineqvlem  9169  mapfien2  9315  supeq1  9351  supeq2  9354  supeq3  9355  oieq1  9420  oieq2  9421  ordtypecbv  9425  ordtypelem3  9428  harval  9468  inf3lema  9536  wemapwe  9609  oef1o  9610  tz9.12lem3  9704  rankvalb  9712  rankvalg  9732  ranksnb  9742  rankonidlem  9743  cardval3  9867  cardidm  9874  alephsuc2  9993  coftr  10186  fin1a2lem11  10323  fin1a2lem12  10324  hsmex  10345  axdc3lem2  10364  zorn2lem1  10409  zorn2lem6  10414  zorn2lem7  10415  zorn2g  10416  wuncval  10656  tskmval  10753  peano5uzti  12610  uzval  12781  rpnnen1  12924  ixxval  13297  fzval  13454  hashbclem  14405  hashbc  14406  shftfn  15026  bitsfval  16383  sadfval  16412  sadcom  16423  smufval  16437  smupp1  16440  smupval  16448  smumullem  16452  gcdval  16456  bezoutlem2  16500  bezoutlem4  16502  lcmval  16552  lcmfval  16581  lcmf0val  16582  lcmfpr  16587  isprm  16633  odzval  16753  pcval  16806  pceulem  16807  pceu  16808  pczpre  16809  pcdiv  16814  prmreclem1  16878  prmreclem4  16881  prmreclem5  16882  ramval  16970  cshws0  17063  imasdsval  17470  mrcval  17567  eldmcoa  18023  chneq1  18569  cycsubg2  19176  cntzval  19287  cntzsnval  19290  odfval  19498  odfvalALT  19499  odval  19500  gexval  19544  efgsfo  19705  dprdval  19971  ablfac1a  20037  ablfac1b  20038  ablfac1eu  20041  ablfaclem1  20053  ablfaclem3  20055  rnghmval  20411  rgspnval  20580  lspval  20961  ocvval  21657  dsmmelbas  21729  frlmsslss  21764  aspval  21862  psrass1lem  21922  psrmulval  21933  mplmonmul  22024  mhpval  22115  mhpmulcl  22125  coe1mul2  22244  pmatcoe1fsupp  22676  istopon  22887  toponsspwpw  22897  clsval  23012  neival  23077  ordtbaslem  23163  ordtbas2  23166  ordtopn1  23169  ordtopn2  23170  cnpval  23211  llyeq  23445  nllyeq  23446  ptfinfin  23494  finlocfin  23495  dissnlocfin  23504  locfindis  23505  xkoopn  23564  kqfval  23698  tsmsfbas  24103  blvalps  24360  blval  24361  nmofval  24689  nmoval  24690  ishtpy  24949  minveclem3b  25405  minveclem3  25406  minveclem4  25409  minveclem5  25410  ovolval  25450  vitalilem2  25586  vitalilem3  25587  vitalilem4  25588  vitali  25590  itg2monolem1  25727  elcpn  25911  mdegmullem  26053  elqaalem1  26296  elqaalem2  26297  elqaalem3  26298  elqaa  26299  aannenlem1  26305  aannenlem2  26306  jensen  26966  vmaval  27090  muval  27109  sgmval  27119  fsumdvdscom  27162  musum  27168  muinv  27170  dchrisum0fval  27482  dchrisum0ff  27484  logsqvma2  27520  pntrlog2bndlem1  27554  cutsval  27786  bdayons  28282  tglngval  28633  ttgval  28957  ttgitvval  28964  ebtwntg  29065  numedglnl  29227  dfnbgr2  29420  dfnbgr3  29421  uvtxusgr  29485  vtxdgval  29552  rusgrnumwrdl2  29670  iswwlksnon  29936  rusgrnumwwlks  30060  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  clwlknf1oclwwlknlem2  30167  clwwlknon  30175  clwwlk0on0  30177  eupth2  30324  fusgreg2wsplem  30418  fusgreghash2wsp  30423  numclwlk1lem1  30454  sspval  30809  ubthlem1  30956  ubthlem2  30957  ubthlem3  30958  ocval  31366  spanval  31419  chsupid  31498  eigvecval  31982  specval  31984  iunpreima  32649  fcobijfs2  32810  pwrssmgc  33075  fxpgaval  33243  nsgqusf1olem3  33490  mplvrpmrhm  33706  psrmonmul  33709  esplyfval  33722  esplyfval0  33723  minplyval  33865  constrsuc  33898  constrcbvlem  33915  crefeq  34005  zarcls1  34029  zarclsun  34030  zarclsiin  34031  zarclsint  34032  zarclssn  34033  zartop  34036  zartopon  34037  zart0  34039  zarmxt1  34040  zarcmp  34042  rhmpreimacnlem  34044  rhmpreimacn  34045  ordtcnvNEW  34080  ordtrest2NEW  34083  ordtconnlem1  34084  measvuni  34374  brfae  34408  omsfval  34454  orvcelval  34629  ballotlemi  34661  bnj602  35073  fineqvnttrclselem2  35282  fineqvnttrclselem3  35283  fineqvnttrclse  35284  onvf1odlem3  35303  subfacp1lem6  35383  kur14  35414  cvmscbv  35456  cvmsi  35463  cvmsval  35464  snmlval  35529  snmlflim  35530  satfv0  35556  satfv1  35561  satfv0fun  35569  satffunlem1lem1  35600  satffunlem2lem1  35602  satfv0fvfmla0  35611  satfv1fvfmla1  35621  prv1n  35629  fvray  36339  fwddifnval  36361  neibastop3  36560  weiunlem  36661  icoreval  37683  fin2so  37942  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem32  37987  ftc1anclem6  38033  islinei  40200  pmapval  40217  paddval  40258  paddcom  40273  pclvalN  40350  ldilset  40569  dilsetN  40613  diafval  41491  diaval  41492  docavalN  41583  dicfval  41635  dochfval  41810  dochval  41811  mapdval  42088  mapdsn2  42102  grpods  42647  unitscyglem1  42648  unitscyglem2  42649  unitscyglem3  42650  unitscyglem4  42651  prjcrvval  43079  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  eldioph4i  43258  diophren  43259  pell1qrval  43292  pell14qrval  43294  pell1234qrval  43296  rpnnen3  43478  fnwe2lem1  43496  pwssplit4  43535  pwslnmlem2  43539  dgraaval  43590  itgoval  43607  proot1hash  43641  rp-intrabeq  43667  rp-unirabeq  43668  rfovfvd  44447  rfovfvfvd  44448  rfovcnvf1od  44449  fsovrfovd  44454  fsovfvd  44455  fsovfvfvd  44456  fsovcnvlem  44458  nzss  44762  supminfxr  45910  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  dvnprod  46395  stoweidlem26  46472  stoweidlem27  46473  stoweidlem31  46477  stoweidlem34  46480  stoweidlem46  46492  fourierdlem79  46631  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem105  46657  fourierdlem107  46659  fourierdlem108  46660  fourierdlem110  46662  etransclem11  46691  salgenval  46767  subsaliuncl  46804  ovnval  46987  ovnval2  46991  ovnval2b  46998  ovncvrrp  47010  ovnsubaddlem1  47016  ovnsubadd  47018  ovncvr2  47057  hspmbl  47075  ovolval2  47090  ovnovollem3  47104  salpreimagelt  47153  salpreimalegt  47155  salpreimagtge  47171  salpreimaltle  47172  issmflem  47173  issmf  47174  salpreimagtlt  47176  smfpreimalt  47177  smfpreimaltf  47182  issmfle  47191  smfpimltxr  47193  smfpreimale  47200  issmfgt  47202  smfpreimagt  47208  issmfge  47216  smflimlem3  47219  smflimlem4  47220  smflim  47223  smfpimgtxr  47226  smfpreimage  47228  fvmptrabdm  47753  elsetpreimafveq  47869  prmdvdsfmtnof1  48062  fppr  48214  dfclnbgr2  48311  dfclnbgr3  48314  dfsclnbgr6  48346  grlimedgclnbgr  48483  grlimgrtri  48491  grilcbri2  48499  bigoval  49037  line  49220  rrxline  49222  sphere  49235  line2y  49243  inpw  49312