Theorem rabbidv 3415

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  {crab 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-rab 3074

This theorem is referenced by:  rabeqbidv  3421  difeq2  4052  seex  5552  mptiniseg  6147  dfpred3g  6218  elovmporab  7524  elovmpt3rab1  7538  fineqvlem  9046  mapfien2  9177  supeq1  9213  supeq2  9216  supeq3  9217  oieq1  9280  oieq2  9281  ordtypecbv  9285  ordtypelem3  9288  harval  9328  inf3lema  9391  wemapwe  9464  oef1o  9465  tz9.12lem3  9556  rankvalb  9564  rankvalg  9584  ranksnb  9594  rankonidlem  9595  cardval3  9719  cardidm  9726  alephsuc2  9845  coftr  10038  fin1a2lem11  10175  fin1a2lem12  10176  hsmex  10197  axdc3lem2  10216  zorn2lem1  10261  zorn2lem6  10266  zorn2lem7  10267  zorn2g  10268  wuncval  10507  tskmval  10604  peano5uzti  12419  uzval  12593  rpnnen1  12732  ixxval  13096  fzval  13250  hashbclem  14173  hashbc  14174  shftfn  14793  bitsfval  16139  sadfval  16168  sadcom  16179  smufval  16193  smupp1  16196  smupval  16204  smumullem  16208  gcdval  16212  bezoutlem2  16257  bezoutlem4  16259  lcmval  16306  lcmfval  16335  lcmf0val  16336  lcmfpr  16341  isprm  16387  odzval  16501  pcval  16554  pceulem  16555  pceu  16556  pczpre  16557  pcdiv  16562  prmreclem1  16626  prmreclem4  16629  prmreclem5  16630  ramval  16718  cshws0  16812  imasdsval  17235  mrcval  17328  eldmcoa  17789  cycsubg2  18838  cntzval  18936  cntzsnval  18939  odfval  19149  odfvalALT  19150  odval  19151  gexval  19192  efgsfo  19354  dprdval  19615  ablfac1a  19681  ablfac1b  19682  ablfac1eu  19685  ablfaclem1  19697  ablfaclem3  19699  lspval  20246  ocvval  20881  dsmmelbas  20955  frlmsslss  20990  aspval  21086  psrass1lemOLD  21152  psrass1lem  21155  psrmulval  21164  mplmonmul  21246  mhpval  21339  mhpmulcl  21348  coe1mul2  21449  pmatcoe1fsupp  21859  istopon  22070  toponsspwpw  22080  clsval  22197  neival  22262  ordtbaslem  22348  ordtbas2  22351  ordtopn1  22354  ordtopn2  22355  cnpval  22396  llyeq  22630  nllyeq  22631  ptfinfin  22679  finlocfin  22680  dissnlocfin  22689  locfindis  22690  xkoopn  22749  kqfval  22883  tsmsfbas  23288  blvalps  23547  blval  23548  nmofval  23887  nmoval  23888  ishtpy  24144  minveclem3b  24601  minveclem3  24602  minveclem4  24605  minveclem5  24606  ovolval  24646  vitalilem2  24782  vitalilem3  24783  vitalilem4  24784  vitali  24786  itg2monolem1  24924  elcpn  25107  mdegmullem  25252  elqaalem1  25488  elqaalem2  25489  elqaalem3  25490  elqaa  25491  aannenlem1  25497  aannenlem2  25498  jensen  26147  vmaval  26271  muval  26290  sgmval  26300  fsumdvdscom  26343  musum  26349  muinv  26351  dchrisum0fval  26662  dchrisum0ff  26664  logsqvma2  26700  pntrlog2bndlem1  26734  tglngval  26921  ttgval  27245  ttgvalOLD  27246  ttgitvval  27258  ebtwntg  27359  numedglnl  27523  dfnbgr2  27713  dfnbgr3  27714  uvtxusgr  27778  vtxdgval  27844  rusgrnumwrdl2  27962  iswwlksnon  28227  rusgrnumwwlks  28348  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwlknf1oclwwlknlem2  28455  clwwlknon  28463  clwwlk0on0  28465  eupth2  28612  fusgreg2wsplem  28706  fusgreghash2wsp  28711  numclwlk1lem1  28742  sspval  29094  ubthlem1  29241  ubthlem2  29242  ubthlem3  29243  ocval  29651  spanval  29704  chsupid  29783  eigvecval  30267  specval  30269  iunpreima  30913  pwrssmgc  31287  nsgqusf1olem3  31609  crefeq  31804  zarcls1  31828  zarclsun  31829  zarclsiin  31830  zarclsint  31831  zarclssn  31832  zartop  31835  zartopon  31836  zart0  31838  zarmxt1  31839  zarcmp  31841  rhmpreimacnlem  31843  rhmpreimacn  31844  ordtcnvNEW  31879  ordtrest2NEW  31882  ordtconnlem1  31883  measvuni  32191  brfae  32225  omsfval  32270  orvcelval  32444  ballotlemi  32476  bnj602  32904  subfacp1lem6  33156  kur14  33187  cvmscbv  33229  cvmsi  33236  cvmsval  33237  snmlval  33302  snmlflim  33303  satfv0  33329  satfv1  33334  satfv0fun  33342  satffunlem1lem1  33373  satffunlem2lem1  33375  satfv0fvfmla0  33384  satfv1fvfmla1  33394  prv1n  33402  naddcllem  33840  naddov2  33843  naddcom  33844  naddid1  33845  scutval  34003  fvray  34452  fwddifnval  34474  neibastop3  34560  icoreval  35533  fin2so  35773  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem32  35818  ftc1anclem6  35864  islinei  37761  pmapval  37778  paddval  37819  paddcom  37834  pclvalN  37911  ldilset  38130  dilsetN  38174  diafval  39052  diaval  39053  docavalN  39144  dicfval  39196  dochfval  39371  dochval  39372  mapdval  39649  mapdsn2  39663  prjcrvval  40476  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  eldioph4i  40641  diophren  40642  pell1qrval  40675  pell14qrval  40677  pell1234qrval  40679  rpnnen3  40861  fnwe2lem1  40882  pwssplit4  40921  pwslnmlem2  40925  dgraaval  40976  itgoval  40993  rgspnval  41000  proot1hash  41032  rfovfvd  41617  rfovfvfvd  41618  rfovcnvf1od  41619  fsovrfovd  41624  fsovfvd  41625  fsovfvfvd  41626  fsovcnvlem  41628  nzss  41942  supminfxr  43011  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  dvnprod  43497  stoweidlem26  43574  stoweidlem27  43575  stoweidlem31  43579  stoweidlem34  43582  stoweidlem46  43594  fourierdlem79  43733  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem105  43759  fourierdlem107  43761  fourierdlem108  43762  fourierdlem110  43764  etransclem11  43793  salgenval  43869  subsaliuncl  43904  ovnval  44086  ovnval2  44090  ovnval2b  44097  ovncvrrp  44109  ovnsubaddlem1  44115  ovnsubadd  44117  ovncvr2  44156  hspmbl  44174  ovolval2  44189  ovnovollem3  44203  salpreimagelt  44252  salpreimalegt  44254  salpreimagtge  44270  salpreimaltle  44271  issmflem  44272  issmf  44273  salpreimagtlt  44275  smfpreimalt  44276  smfpreimaltf  44281  issmfle  44290  smfpimltxr  44292  smfpreimale  44299  issmfgt  44301  smfpreimagt  44307  issmfge  44315  smflimlem3  44318  smflimlem4  44319  smflim  44322  smfpimgtxr  44325  smfpreimage  44327  fvmptrabdm  44796  elsetpreimafveq  44860  prmdvdsfmtnof1  45050  fppr  45189  rnghmval  45460  bigoval  45906  line  46089  rrxline  46091  sphere  46104  line2y  46112  inpw  46175