Theorem rabbidv 3164

Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (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 3163	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {crab 2900

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  df-ral 2901  df-rab 2905

This theorem is referenced by:  rabeqbidv  3168  difeq2  3684  seex  5001  mptiniseg  5546  dfpred3g  5608  elovmpt2rab  6778  elovmpt3rab1  6791  fineqvlem  8059  mapfien2  8197  supeq1  8234  supeq2  8237  supeq3  8238  oieq1  8300  oieq2  8301  ordtypecbv  8305  ordtypelem3  8308  harval  8350  inf3lema  8404  wemapwe  8477  oef1o  8478  tz9.12lem3  8535  rankvalb  8543  rankvalg  8563  ranksnb  8573  rankonidlem  8574  cardval3  8661  cardidm  8668  alephsuc2  8786  coftr  8978  fin1a2lem11  9115  fin1a2lem12  9116  hsmex  9137  axdc3lem2  9156  zorn2lem1  9201  zorn2lem6  9206  zorn2lem7  9207  zorn2g  9208  wuncval  9443  tskmval  9540  peano5uzti  11343  uzval  11565  rpnnen1  11696  ixxval  12054  fzval  12199  hashbclem  13093  hashbc  13094  shftfn  13661  bitsfval  14983  sadfval  15012  sadcom  15023  smufval  15037  smupp1  15040  smupval  15048  smumullem  15052  gcdval  15056  bezoutlem2  15095  bezoutlem4  15097  lcmval  15143  lcmfval  15172  lcmf0val  15173  lcmfpr  15178  isprm  15225  isprm2lem  15232  odzval  15334  pcval  15387  pceulem  15388  pceu  15389  pczpre  15390  pcdiv  15395  prmreclem1  15458  prmreclem4  15461  prmreclem5  15462  ramval  15550  cshws0  15646  imasdsval  15998  mrcval  16093  eldmcoa  16538  cycsubg2  17454  cntzval  17577  cntzsnval  17580  odfval  17775  odval  17776  gexval  17816  efgsfo  17975  dprdval  18225  ablfac1a  18291  ablfac1b  18292  ablfac1eu  18295  ablfaclem1  18307  ablfaclem3  18309  lspval  18796  aspval  19149  psrass1lem  19198  psrmulval  19207  mplmonmul  19285  coe1mul2  19460  ocvval  19830  dsmmelbas  19902  frlmsslss  19932  pmatcoe1fsupp  20325  istopon  20540  clsval  20651  neival  20716  ordtbaslem  20802  ordtbas2  20805  ordtopn1  20808  ordtopn2  20809  cnpval  20850  llyeq  21083  nllyeq  21084  ptfinfin  21132  finlocfin  21133  dissnlocfin  21142  locfindis  21143  xkoopn  21202  kqfval  21336  tsmsfbas  21741  blvalps  22000  blval  22001  nmofval  22328  nmoval  22329  ishtpy  22579  minveclem3b  23007  minveclem3  23008  minveclem4  23011  minveclem5  23012  ovolval  23049  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  vitali  23188  itg2monolem1  23323  elcpn  23503  mdegmullem  23642  elqaalem1  23878  elqaalem2  23879  elqaalem3  23880  elqaa  23881  aannenlem1  23887  aannenlem2  23888  jensen  24515  vmaval  24639  muval  24658  sgmval  24668  fsumdvdscom  24711  musum  24717  muinv  24719  dchrisum0fval  24994  dchrisum0ff  24996  logsqvma2  25032  pntrlog2bndlem1  25066  tglngval  25246  ttgval  25555  ttgitvval  25562  ebtwntg  25662  nbgraopALT  25953  nbgraop1  25954  wwlkn  26210  clwwlkn  26295  hashecclwwlkn1  26361  usghashecclwwlk  26362  2wlkonot  26392  2spthonot  26393  2pthwlkonot  26412  vdgrval  26423  rusgraprop4  26471  rusgrasn  26472  rusgranumwwlkl1  26473  rusgranumwlklem1  26476  rusgranumwlklem3  26478  rusgranumwlks  26483  rusgranumwlkg  26485  eupath2  26507  usg2spot2nb  26592  usgreg2spot  26594  2spotmdisj  26595  usgreghash2spot  26596  numclwwlkun  26606  numclwwlkdisj  26607  numclwwlk3lem  26635  numclwwlk5  26639  sspval  26962  ubthlem1  27110  ubthlem2  27111  ubthlem3  27112  ocval  27523  spanval  27576  chsupid  27655  eigvecval  28139  specval  28141  iunpreima  28765  aciunf1  28845  crefeq  29240  ordtcnvNEW  29294  ordtrest2NEW  29297  ordtconlem1  29298  measvuni  29604  brfae  29638  omsfval  29683  orvcelval  29857  ballotlemi  29889  bnj602  30239  subfacp1lem6  30421  kur14  30452  cvmscbv  30494  cvmsi  30501  cvmsval  30502  snmlval  30567  snmlflim  30568  fvray  31418  fwddifnval  31440  neibastop3  31527  bj-toponss  32241  icoreval  32377  fin2so  32566  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem32  32611  ftc1anclem6  32660  islinei  34044  pmapval  34061  paddval  34102  paddcom  34117  pclvalN  34194  ldilset  34413  dilsetN  34458  diafval  35338  diaval  35339  docavalN  35430  dicfval  35482  dochfval  35657  dochval  35658  mapdval  35935  mapdsn2  35949  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  eldioph4i  36394  diophren  36395  pell1qrval  36428  pell14qrval  36430  pell1234qrval  36432  rpnnen3  36617  fnwe2lem1  36638  pwssplit4  36677  pwslnmlem2  36681  dgraaval  36733  itgoval  36750  rgspnval  36757  proot1hash  36797  rfovfvd  37316  rfovfvfvd  37317  rfovcnvf1od  37318  fsovrfovd  37323  fsovfvd  37324  fsovfvfvd  37325  fsovcnvlem  37327  nzss  37538  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  dvnprod  38839  stoweidlem26  38919  stoweidlem27  38920  stoweidlem31  38924  stoweidlem34  38927  stoweidlem46  38939  fourierdlem79  39078  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem105  39104  fourierdlem107  39106  fourierdlem108  39107  fourierdlem110  39109  etransclem11  39138  salgenval  39217  subsaliuncl  39252  ovnval  39431  ovnval2  39435  ovnval2b  39442  ovncvrrp  39454  ovnsubaddlem1  39460  ovnsubadd  39462  ovncvr2  39501  hspmbl  39519  ovolval2  39534  ovnovollem3  39548  salpreimagelt  39595  salpreimalegt  39597  salpreimagtge  39611  salpreimaltle  39612  issmflem  39613  issmf  39614  salpreimagtlt  39616  smfpreimalt  39617  smfpreimaltf  39623  issmfle  39632  smfpimltxr  39634  smfpreimale  39641  issmfgt  39643  smfpreimagt  39648  issmfge  39656  smflimlem3  39659  smflimlem4  39660  smflim  39663  smfpimgtxr  39666  smfpreimage  39668  prmdvdsfmtnof1  40037  dfnbgr2  40561  dfnbgr3  40562  uvtxusgr  40629  vtxdgval  40684  rusgrnumwrdl2  40786  iswwlksnon  41051  wwlks2onv  41158  rusgrnumwwlks  41177  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwwlksndisj  41280  eupth2  41407  fusgr2wsp2nb  41498  fusgreg2wsp  41500  2wspmdisj  41501  fusgreghash2wsp  41502  av-numclwwlk3lem  41538  av-numclwwlk5  41542  rnghmval  41681  bigoval  42141