Theorem rabbidv 3420

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1520   ∈ wcel 2079  {crab 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-ral 3108  df-rab 3112

This theorem is referenced by:  rabeqbidv  3425  difeq2  4009  seex  5398  mptiniseg  5960  dfpred3g  6026  elovmporab  7241  elovmpt3rab1  7254  suppcofnd  7713  fineqvlem  8568  mapfien2  8708  supeq1  8745  supeq2  8748  supeq3  8749  oieq1  8812  oieq2  8813  ordtypecbv  8817  ordtypelem3  8820  harval  8862  inf3lema  8922  wemapwe  8995  oef1o  8996  tz9.12lem3  9053  rankvalb  9061  rankvalg  9081  ranksnb  9091  rankonidlem  9092  cardval3  9216  cardidm  9223  alephsuc2  9341  coftr  9530  fin1a2lem11  9667  fin1a2lem12  9668  hsmex  9689  axdc3lem2  9708  zorn2lem1  9753  zorn2lem6  9758  zorn2lem7  9759  zorn2g  9760  wuncval  9999  tskmval  10096  peano5uzti  11910  uzval  12084  rpnnen1  12221  ixxval  12585  fzval  12733  hashbclem  13646  hashbc  13647  shftfn  14254  bitsfval  15593  sadfval  15622  sadcom  15633  smufval  15647  smupp1  15650  smupval  15658  smumullem  15662  gcdval  15666  bezoutlem2  15705  bezoutlem4  15707  lcmval  15753  lcmfval  15782  lcmf0val  15783  lcmfpr  15788  isprm  15834  odzval  15945  pcval  15998  pceulem  15999  pceu  16000  pczpre  16001  pcdiv  16006  prmreclem1  16069  prmreclem4  16072  prmreclem5  16073  ramval  16161  cshws0  16252  imasdsval  16605  mrcval  16698  eldmcoa  17142  cycsubg2  18058  cntzval  18180  cntzsnval  18183  odfval  18379  odfvalALT  18380  odval  18381  gexval  18421  efgsfo  18580  dprdval  18830  ablfac1a  18896  ablfac1b  18897  ablfac1eu  18900  ablfaclem1  18912  ablfaclem3  18914  lspval  19425  aspval  19778  psrass1lem  19833  psrmulval  19842  mplmonmul  19920  mhpval  20004  coe1mul2  20108  ocvval  20481  dsmmelbas  20553  frlmsslss  20588  pmatcoe1fsupp  20981  istopon  21192  toponsspwpw  21202  clsval  21317  neival  21382  ordtbaslem  21468  ordtbas2  21471  ordtopn1  21474  ordtopn2  21475  cnpval  21516  llyeq  21750  nllyeq  21751  ptfinfin  21799  finlocfin  21800  dissnlocfin  21809  locfindis  21810  xkoopn  21869  kqfval  22003  tsmsfbas  22407  blvalps  22666  blval  22667  nmofval  22994  nmoval  22995  ishtpy  23247  minveclem3b  23702  minveclem3  23703  minveclem4  23706  minveclem5  23707  ovolval  23745  vitalilem2  23881  vitalilem3  23882  vitalilem4  23883  vitali  23885  itg2monolem1  24022  elcpn  24202  mdegmullem  24343  elqaalem1  24579  elqaalem2  24580  elqaalem3  24581  elqaa  24582  aannenlem1  24588  aannenlem2  24589  jensen  25236  vmaval  25360  muval  25379  sgmval  25389  fsumdvdscom  25432  musum  25438  muinv  25440  dchrisum0fval  25751  dchrisum0ff  25753  logsqvma2  25789  pntrlog2bndlem1  25823  tglngval  26007  ttgval  26332  ttgitvval  26339  ebtwntg  26439  numedglnl  26600  dfnbgr2  26790  dfnbgr3  26791  uvtxusgr  26855  vtxdgval  26921  rusgrnumwrdl2  27039  iswwlksnon  27306  rusgrnumwwlks  27428  hashecclwwlkn1  27531  umgrhashecclwwlk  27532  clwlknf1oclwwlknlem2  27536  clwwlknon  27544  clwwlk0on0  27546  eupth2  27694  fusgreg2wsplem  27792  fusgreghash2wsp  27797  numclwlk1lem1  27828  sspval  28179  ubthlem1  28326  ubthlem2  28327  ubthlem3  28328  ocval  28736  spanval  28789  chsupid  28868  eigvecval  29352  specval  29354  iunpreima  29985  crefeq  30682  ordtcnvNEW  30736  ordtrest2NEW  30739  ordtconnlem1  30740  measvuni  31046  brfae  31080  omsfval  31125  orvcelval  31299  ballotlemi  31331  bnj602  31759  subfacp1lem6  31996  kur14  32027  cvmscbv  32069  cvmsi  32076  cvmsval  32077  snmlval  32142  snmlflim  32143  satfv0  32169  satfv0fun  32180  satffunlem1lem1  32210  satffunlem2lem1  32212  satfv0fvfmla0  32221  scutval  32819  fvray  33156  fwddifnval  33178  neibastop3  33264  icoreval  34111  fin2so  34356  poimirlem26  34395  poimirlem27  34396  poimirlem28  34397  poimirlem32  34401  ftc1anclem6  34449  islinei  36357  pmapval  36374  paddval  36415  paddcom  36430  pclvalN  36507  ldilset  36726  dilsetN  36770  diafval  37648  diaval  37649  docavalN  37740  dicfval  37792  dochfval  37967  dochval  37968  mapdval  38245  mapdsn2  38259  2rexfrabdioph  38829  3rexfrabdioph  38830  4rexfrabdioph  38831  6rexfrabdioph  38832  7rexfrabdioph  38833  eldioph4i  38845  diophren  38846  pell1qrval  38879  pell14qrval  38881  pell1234qrval  38883  rpnnen3  39065  fnwe2lem1  39086  pwssplit4  39125  pwslnmlem2  39129  dgraaval  39180  itgoval  39197  rgspnval  39204  proot1hash  39236  rfovfvd  39784  rfovfvfvd  39785  rfovcnvf1od  39786  fsovrfovd  39791  fsovfvd  39792  fsovfvfvd  39793  fsovcnvlem  39795  nzss  40139  supminfxr  41236  dvnprodlem1  41726  dvnprodlem2  41727  dvnprodlem3  41728  dvnprod  41729  stoweidlem26  41807  stoweidlem27  41808  stoweidlem31  41812  stoweidlem34  41815  stoweidlem46  41827  fourierdlem79  41966  fourierdlem96  41983  fourierdlem97  41984  fourierdlem98  41985  fourierdlem99  41986  fourierdlem105  41992  fourierdlem107  41994  fourierdlem108  41995  fourierdlem110  41997  etransclem11  42026  salgenval  42102  subsaliuncl  42137  ovnval  42319  ovnval2  42323  ovnval2b  42330  ovncvrrp  42342  ovnsubaddlem1  42348  ovnsubadd  42350  ovncvr2  42389  hspmbl  42407  ovolval2  42422  ovnovollem3  42436  salpreimagelt  42482  salpreimalegt  42484  salpreimagtge  42498  salpreimaltle  42499  issmflem  42500  issmf  42501  salpreimagtlt  42503  smfpreimalt  42504  smfpreimaltf  42509  issmfle  42518  smfpimltxr  42520  smfpreimale  42527  issmfgt  42529  smfpreimagt  42534  issmfge  42542  smflimlem3  42545  smflimlem4  42546  smflim  42549  smfpimgtxr  42552  smfpreimage  42554  fvmptrabdm  42962  prmdvdsfmtnof1  43185  fppr  43327  rnghmval  43594  bigoval  44044  line  44154  rrxline  44156  sphere  44169  line2y  44177