Theorem rabbidva 3435

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.)

Hypothesis

Ref	Expression
rabbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidva	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidva

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 577	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3430	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {crab 3428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-rab 3429

This theorem is referenced by:  rabbidv  3436  rabeqbidva  3445  rabbi2dva  4218  rabxfrd  5419  seinxp  5763  ordintdif  6422  f1oresrab  7140  onsucmin  7828  suppval1  8175  mptsuppd  8196  naddasslem1  8719  naddasslem2  8720  cantnflem1  9718  harsucnn  10027  dfinfre  12231  ixxin  13379  mptnn0fsuppr  14002  scshwfzeqfzo  14815  incexc2  15822  smueqlem  16470  gcdass  16528  lcmass  16590  pcneg  16848  ramval  16982  acsfn  17644  monpropd  17725  f1omvdcnv  19404  pmtrmvd  19416  submod  19529  odngen  19537  sylow3lem6  19592  efgsfo  19699  acsfn1p  20692  rngqiprngimf1  21195  rrgsupp  21243  dsmmbas2  21676  dsmmacl  21680  frlmbas  21694  frlmsslss2  21714  mplsubglem2  21948  ltbwe  21987  coe1mul2lem2  22192  scmatmats  22431  mretopd  23014  ordtbaslem  23110  ordtrest  23124  ordtrest2lem  23125  leordtval  23135  xkopt  23577  xkoco1cn  23579  xkoco2cn  23580  xkoinjcn  23609  r0cld  23660  utopsnneiplem  24170  stdbdbl  24444  minveclem3b  25374  minveclem4  25378  lhop1lem  25964  idomrootle  26125  mumul  27131  sqff1o  27132  lgsquadlem1  27331  lgsquadlem2  27332  2lgslem1a  27342  lrrecse  27877  lrrecpred  27879  elntg2  28814  edglnl  28974  nbupgr  29175  vtxdun  29313  wwlksnextprop  29741  wpthswwlks2on  29790  rusgrnumwwlkslem  29798  rusgrnumwwlks  29803  clwlknf1oclwwlkn  29912  frcond3  30097  extwwlkfab  30180  grpoidinv2  30343  grpoinv  30353  xppreima  32450  qusker  33079  nsgqusf1olem3  33143  fedgmullem2  33333  ply1annidllem  33377  zarclsun  33476  cnvordtrestixx  33519  ordtrestNEW  33527  ordtrest2NEWlem  33528  fnrelpredd  34717  satfv1lem  34977  satefvfmla0  35033  satefvfmla1  35040  lineunray  35748  lineelsb2  35749  linecom  35751  ee7.2aOLD  35950  poimirlem26  37124  poimirlem27  37125  mbfposadd  37145  cnambfre  37146  itg2addnclem2  37150  iblabsnclem  37161  ftc1anclem1  37171  lfl1dim2N  38598  pmapat  39240  pmapglbx  39246  dvhb1dimN  40463  dia0  40529  mapdval2N  41107  mapdsn  41118  hlhilocv  41438  isprimroot  41568  aks6d1c6isolem3  41652  istopclsd  42123  diophren  42236  rabrenfdioph  42237  pwfi2f1o  42523  idomodle  42622  hausgraph  42636  nadd1rabtr  42820  nadd1rabex  42822  nadd1suc  42824  naddsuc2  42825  minregex2  42968  fsovcnvlem  43446  ntrneifv3  43515  ntrneifv4  43518  clsneifv3  43543  clsneifv4  43544  neicvgfv  43554  nzss  43757  preimaiocmnf  44948  preimaicomnf  46101  smfsupxr  46206  smfliminflem  46220  sprvalpwle2  46831  fpprmod  47069  dfsclnbgr2  47183  dfvopnbgr2  47190  rmsupp0  47483  lco0  47546  rrxlinesc  47859  rrxlinec  47860  rrx2line  47864  rrx2vlinest  47865  rrx2linest  47866  rrx2linesl  47867  rrx2linest2  47868  2sphere  47873  2sphere0  47874  line2  47876  itsclinecirc0b  47898