Theorem rabbidv 3440

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3432

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-rab 3433

This theorem is referenced by:  difeq2  4116  seex  5638  mptiniseg  6238  dfpred3g  6312  elovmporab  7654  elovmpt3rab1  7668  naddcllem  8677  naddov2  8680  naddcom  8683  naddrid  8684  naddass  8697  fineqvlem  9264  mapfien2  9406  supeq1  9442  supeq2  9445  supeq3  9446  oieq1  9509  oieq2  9510  ordtypecbv  9514  ordtypelem3  9517  harval  9557  inf3lema  9621  wemapwe  9694  oef1o  9695  tz9.12lem3  9786  rankvalb  9794  rankvalg  9814  ranksnb  9824  rankonidlem  9825  cardval3  9949  cardidm  9956  alephsuc2  10077  coftr  10270  fin1a2lem11  10407  fin1a2lem12  10408  hsmex  10429  axdc3lem2  10448  zorn2lem1  10493  zorn2lem6  10498  zorn2lem7  10499  zorn2g  10500  wuncval  10739  tskmval  10836  peano5uzti  12656  uzval  12828  rpnnen1  12971  ixxval  13336  fzval  13490  hashbclem  14415  hashbc  14416  shftfn  15024  bitsfval  16368  sadfval  16397  sadcom  16408  smufval  16422  smupp1  16425  smupval  16433  smumullem  16437  gcdval  16441  bezoutlem2  16486  bezoutlem4  16488  lcmval  16533  lcmfval  16562  lcmf0val  16563  lcmfpr  16568  isprm  16614  odzval  16728  pcval  16781  pceulem  16782  pceu  16783  pczpre  16784  pcdiv  16789  prmreclem1  16853  prmreclem4  16856  prmreclem5  16857  ramval  16945  cshws0  17039  imasdsval  17465  mrcval  17558  eldmcoa  18019  cycsubg2  19125  cntzval  19226  cntzsnval  19229  odfval  19441  odfvalALT  19442  odval  19443  gexval  19487  efgsfo  19648  dprdval  19914  ablfac1a  19980  ablfac1b  19981  ablfac1eu  19984  ablfaclem1  19996  ablfaclem3  19998  rnghmval  20331  lspval  20730  ocvval  21439  dsmmelbas  21513  frlmsslss  21548  aspval  21646  psrass1lemOLD  21712  psrass1lem  21715  psrmulval  21724  mplmonmul  21810  mhpval  21902  mhpmulcl  21911  coe1mul2  22011  pmatcoe1fsupp  22423  istopon  22634  toponsspwpw  22644  clsval  22761  neival  22826  ordtbaslem  22912  ordtbas2  22915  ordtopn1  22918  ordtopn2  22919  cnpval  22960  llyeq  23194  nllyeq  23195  ptfinfin  23243  finlocfin  23244  dissnlocfin  23253  locfindis  23254  xkoopn  23313  kqfval  23447  tsmsfbas  23852  blvalps  24111  blval  24112  nmofval  24451  nmoval  24452  ishtpy  24712  minveclem3b  25169  minveclem3  25170  minveclem4  25173  minveclem5  25174  ovolval  25214  vitalilem2  25350  vitalilem3  25351  vitalilem4  25352  vitali  25354  itg2monolem1  25492  elcpn  25675  mdegmullem  25820  elqaalem1  26056  elqaalem2  26057  elqaalem3  26058  elqaa  26059  aannenlem1  26065  aannenlem2  26066  jensen  26717  vmaval  26841  muval  26860  sgmval  26870  fsumdvdscom  26913  musum  26919  muinv  26921  dchrisum0fval  27232  dchrisum0ff  27234  logsqvma2  27270  pntrlog2bndlem1  27304  scutval  27526  tglngval  28057  ttgval  28381  ttgvalOLD  28382  ttgitvval  28394  ebtwntg  28495  numedglnl  28659  dfnbgr2  28849  dfnbgr3  28850  uvtxusgr  28914  vtxdgval  28980  rusgrnumwrdl2  29098  iswwlksnon  29362  rusgrnumwwlks  29483  hashecclwwlkn1  29585  umgrhashecclwwlk  29586  clwlknf1oclwwlknlem2  29590  clwwlknon  29598  clwwlk0on0  29600  eupth2  29747  fusgreg2wsplem  29841  fusgreghash2wsp  29846  numclwlk1lem1  29877  sspval  30231  ubthlem1  30378  ubthlem2  30379  ubthlem3  30380  ocval  30788  spanval  30841  chsupid  30920  eigvecval  31404  specval  31406  iunpreima  32051  pwrssmgc  32425  nsgqusf1olem3  32788  minplyval  33043  crefeq  33111  zarcls1  33135  zarclsun  33136  zarclsiin  33137  zarclsint  33138  zarclssn  33139  zartop  33142  zartopon  33143  zart0  33145  zarmxt1  33146  zarcmp  33148  rhmpreimacnlem  33150  rhmpreimacn  33151  ordtcnvNEW  33186  ordtrest2NEW  33189  ordtconnlem1  33190  measvuni  33498  brfae  33532  omsfval  33579  orvcelval  33753  ballotlemi  33785  bnj602  34212  subfacp1lem6  34462  kur14  34493  cvmscbv  34535  cvmsi  34542  cvmsval  34543  snmlval  34608  snmlflim  34609  satfv0  34635  satfv1  34640  satfv0fun  34648  satffunlem1lem1  34679  satffunlem2lem1  34681  satfv0fvfmla0  34690  satfv1fvfmla1  34700  prv1n  34708  fvray  35405  fwddifnval  35427  neibastop3  35550  icoreval  36537  fin2so  36778  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  poimirlem32  36823  ftc1anclem6  36869  islinei  38914  pmapval  38931  paddval  38972  paddcom  38987  pclvalN  39064  ldilset  39283  dilsetN  39327  diafval  40205  diaval  40206  docavalN  40297  dicfval  40349  dochfval  40524  dochval  40525  mapdval  40802  mapdsn2  40816  prjcrvval  41676  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  eldioph4i  41852  diophren  41853  pell1qrval  41886  pell14qrval  41888  pell1234qrval  41890  rpnnen3  42073  fnwe2lem1  42094  pwssplit4  42133  pwslnmlem2  42137  dgraaval  42188  itgoval  42205  rgspnval  42212  proot1hash  42244  rp-intrabeq  42272  rp-unirabeq  42273  rfovfvd  43055  rfovfvfvd  43056  rfovcnvf1od  43057  fsovrfovd  43062  fsovfvd  43063  fsovfvfvd  43064  fsovcnvlem  43066  nzss  43378  supminfxr  44473  dvnprodlem1  44961  dvnprodlem2  44962  dvnprodlem3  44963  dvnprod  44964  stoweidlem26  45041  stoweidlem27  45042  stoweidlem31  45046  stoweidlem34  45049  stoweidlem46  45061  fourierdlem79  45200  fourierdlem96  45217  fourierdlem97  45218  fourierdlem98  45219  fourierdlem99  45220  fourierdlem105  45226  fourierdlem107  45228  fourierdlem108  45229  fourierdlem110  45231  etransclem11  45260  salgenval  45336  subsaliuncl  45373  ovnval  45556  ovnval2  45560  ovnval2b  45567  ovncvrrp  45579  ovnsubaddlem1  45585  ovnsubadd  45587  ovncvr2  45626  hspmbl  45644  ovolval2  45659  ovnovollem3  45673  salpreimagelt  45722  salpreimalegt  45724  salpreimagtge  45740  salpreimaltle  45741  issmflem  45742  issmf  45743  salpreimagtlt  45745  smfpreimalt  45746  smfpreimaltf  45751  issmfle  45760  smfpimltxr  45762  smfpreimale  45769  issmfgt  45771  smfpreimagt  45777  issmfge  45785  smflimlem3  45788  smflimlem4  45789  smflim  45792  smfpimgtxr  45795  smfpreimage  45797  fvmptrabdm  46300  elsetpreimafveq  46364  prmdvdsfmtnof1  46554  fppr  46693  bigoval  47323  line  47506  rrxline  47508  sphere  47521  line2y  47529  inpw  47591