Theorem rabbidv 3483

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 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3481	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536   ∈ wcel 2113  {crab 3145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-rab 3150

This theorem is referenced by:  rabeqbidv  3488  difeq2  4096  seex  5521  mptiniseg  6096  dfpred3g  6162  elovmporab  7394  elovmpt3rab1  7408  suppcofnd  7874  fineqvlem  8735  mapfien2  8875  supeq1  8912  supeq2  8915  supeq3  8916  oieq1  8979  oieq2  8980  ordtypecbv  8984  ordtypelem3  8987  harval  9029  inf3lema  9090  wemapwe  9163  oef1o  9164  tz9.12lem3  9221  rankvalb  9229  rankvalg  9249  ranksnb  9259  rankonidlem  9260  cardval3  9384  cardidm  9391  alephsuc2  9509  coftr  9698  fin1a2lem11  9835  fin1a2lem12  9836  hsmex  9857  axdc3lem2  9876  zorn2lem1  9921  zorn2lem6  9926  zorn2lem7  9927  zorn2g  9928  wuncval  10167  tskmval  10264  peano5uzti  12075  uzval  12248  rpnnen1  12385  ixxval  12749  fzval  12897  hashbclem  13813  hashbc  13814  shftfn  14435  bitsfval  15775  sadfval  15804  sadcom  15815  smufval  15829  smupp1  15832  smupval  15840  smumullem  15844  gcdval  15848  bezoutlem2  15891  bezoutlem4  15893  lcmval  15939  lcmfval  15968  lcmf0val  15969  lcmfpr  15974  isprm  16020  odzval  16131  pcval  16184  pceulem  16185  pceu  16186  pczpre  16187  pcdiv  16192  prmreclem1  16255  prmreclem4  16258  prmreclem5  16259  ramval  16347  cshws0  16438  imasdsval  16791  mrcval  16884  eldmcoa  17328  cycsubg2  18356  cntzval  18454  cntzsnval  18457  odfval  18663  odfvalALT  18664  odval  18665  gexval  18706  efgsfo  18868  dprdval  19128  ablfac1a  19194  ablfac1b  19195  ablfac1eu  19198  ablfaclem1  19210  ablfaclem3  19212  lspval  19750  aspval  20105  psrass1lem  20160  psrmulval  20169  mplmonmul  20248  mhpval  20336  coe1mul2  20440  ocvval  20814  dsmmelbas  20886  frlmsslss  20921  pmatcoe1fsupp  21312  istopon  21523  toponsspwpw  21533  clsval  21648  neival  21713  ordtbaslem  21799  ordtbas2  21802  ordtopn1  21805  ordtopn2  21806  cnpval  21847  llyeq  22081  nllyeq  22082  ptfinfin  22130  finlocfin  22131  dissnlocfin  22140  locfindis  22141  xkoopn  22200  kqfval  22334  tsmsfbas  22739  blvalps  22998  blval  22999  nmofval  23326  nmoval  23327  ishtpy  23579  minveclem3b  24034  minveclem3  24035  minveclem4  24038  minveclem5  24039  ovolval  24077  vitalilem2  24213  vitalilem3  24214  vitalilem4  24215  vitali  24217  itg2monolem1  24354  elcpn  24534  mdegmullem  24675  elqaalem1  24911  elqaalem2  24912  elqaalem3  24913  elqaa  24914  aannenlem1  24920  aannenlem2  24921  jensen  25569  vmaval  25693  muval  25712  sgmval  25722  fsumdvdscom  25765  musum  25771  muinv  25773  dchrisum0fval  26084  dchrisum0ff  26086  logsqvma2  26122  pntrlog2bndlem1  26156  tglngval  26340  ttgval  26664  ttgitvval  26671  ebtwntg  26771  numedglnl  26932  dfnbgr2  27122  dfnbgr3  27123  uvtxusgr  27187  vtxdgval  27253  rusgrnumwrdl2  27371  iswwlksnon  27634  rusgrnumwwlks  27756  hashecclwwlkn1  27859  umgrhashecclwwlk  27860  clwlknf1oclwwlknlem2  27864  clwwlknon  27872  clwwlk0on0  27874  eupth2  28021  fusgreg2wsplem  28115  fusgreghash2wsp  28120  numclwlk1lem1  28151  sspval  28503  ubthlem1  28650  ubthlem2  28651  ubthlem3  28652  ocval  29060  spanval  29113  chsupid  29192  eigvecval  29676  specval  29678  iunpreima  30319  crefeq  31113  ordtcnvNEW  31167  ordtrest2NEW  31170  ordtconnlem1  31171  measvuni  31477  brfae  31511  omsfval  31556  orvcelval  31730  ballotlemi  31762  bnj602  32191  subfacp1lem6  32436  kur14  32467  cvmscbv  32509  cvmsi  32516  cvmsval  32517  snmlval  32582  snmlflim  32583  satfv0  32609  satfv1  32614  satfv0fun  32622  satffunlem1lem1  32653  satffunlem2lem1  32655  satfv0fvfmla0  32664  satfv1fvfmla1  32674  prv1n  32682  scutval  33269  fvray  33606  fwddifnval  33628  neibastop3  33714  icoreval  34638  fin2so  34883  poimirlem26  34922  poimirlem27  34923  poimirlem28  34924  poimirlem32  34928  ftc1anclem6  34976  islinei  36880  pmapval  36897  paddval  36938  paddcom  36953  pclvalN  37030  ldilset  37249  dilsetN  37293  diafval  38171  diaval  38172  docavalN  38263  dicfval  38315  dochfval  38490  dochval  38491  mapdval  38768  mapdsn2  38782  2rexfrabdioph  39399  3rexfrabdioph  39400  4rexfrabdioph  39401  6rexfrabdioph  39402  7rexfrabdioph  39403  eldioph4i  39415  diophren  39416  pell1qrval  39449  pell14qrval  39451  pell1234qrval  39453  rpnnen3  39635  fnwe2lem1  39656  pwssplit4  39695  pwslnmlem2  39699  dgraaval  39750  itgoval  39767  rgspnval  39774  proot1hash  39806  rfovfvd  40354  rfovfvfvd  40355  rfovcnvf1od  40356  fsovrfovd  40361  fsovfvd  40362  fsovfvfvd  40363  fsovcnvlem  40365  nzss  40655  supminfxr  41746  dvnprodlem1  42237  dvnprodlem2  42238  dvnprodlem3  42239  dvnprod  42240  stoweidlem26  42318  stoweidlem27  42319  stoweidlem31  42323  stoweidlem34  42326  stoweidlem46  42338  fourierdlem79  42477  fourierdlem96  42494  fourierdlem97  42495  fourierdlem98  42496  fourierdlem99  42497  fourierdlem105  42503  fourierdlem107  42505  fourierdlem108  42506  fourierdlem110  42508  etransclem11  42537  salgenval  42613  subsaliuncl  42648  ovnval  42830  ovnval2  42834  ovnval2b  42841  ovncvrrp  42853  ovnsubaddlem1  42859  ovnsubadd  42861  ovncvr2  42900  hspmbl  42918  ovolval2  42933  ovnovollem3  42947  salpreimagelt  42993  salpreimalegt  42995  salpreimagtge  43009  salpreimaltle  43010  issmflem  43011  issmf  43012  salpreimagtlt  43014  smfpreimalt  43015  smfpreimaltf  43020  issmfle  43029  smfpimltxr  43031  smfpreimale  43038  issmfgt  43040  smfpreimagt  43045  issmfge  43053  smflimlem3  43056  smflimlem4  43057  smflim  43060  smfpimgtxr  43063  smfpreimage  43065  fvmptrabdm  43499  elsetpreimafveq  43564  prmdvdsfmtnof1  43756  fppr  43898  rnghmval  44169  bigoval  44616  line  44726  rrxline  44728  sphere  44741  line2y  44749