Theorem rabbidva 3422

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is referenced by:  rabbidv  3423  rabeqbidva  3432  rabeqbidvaOLD  3433  rabbi2dva  4178  rabxfrd  5388  seinxp  5745  ordintdif  6412  f1oresrab  7123  onsucmin  7813  suppval1  8158  mptsuppd  8179  naddasslem1  8677  naddasslem2  8678  naddsuc2  8684  cantnflem1  9654  harsucnn  9980  dfinfre  12191  ixxin  13384  mptnn0fsuppr  14031  scshwfzeqfzo  14859  incexc2  15888  smueqlem  16543  gcdass  16600  lcmass  16667  pcneg  16929  ramval  17063  acsfn  17710  monpropd  17789  f1omvdcnv  19509  pmtrmvd  19521  submod  19634  odngen  19642  sylow3lem6  19697  efgsfo  19804  rrgsupp  20800  acsfn1p  20902  rngqiprngimf1  21440  dsmmbas2  21887  dsmmacl  21891  frlmbas  21905  frlmsslss2  21925  mplsubglem2  22150  ltbwe  22195  coe1mul2lem2  22429  scmatmats  22668  mretopd  23249  ordtbaslem  23345  ordtrest  23359  ordtrest2lem  23360  leordtval  23370  xkopt  23812  xkoco1cn  23814  xkoco2cn  23815  xkoinjcn  23844  r0cld  23895  utopsnneiplem  24404  stdbdbl  24674  minveclem3b  25587  minveclem4  25591  lhop1lem  26172  idomrootle  26330  mumul  27345  sqff1o  27346  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1a  27555  lrrecse  28135  lrrecpred  28137  plngcplem  29067  elntg2  29335  edglnl  29493  nbupgr  29694  vtxdun  29831  wwlksnextprop  30261  wpthswwlks2on  30313  rusgrnumwwlkslem  30321  rusgrnumwwlks  30326  clwlknf1oclwwlkn  30435  frcond3  30620  extwwlkfab  30703  grpoidinv2  30867  grpoinv  30877  xppreima  32990  qusker  33669  nsgqusf1olem3  33724  fedgmullem2  34020  ply1annidllem  34091  zarclsun  34260  cnvordtrestixx  34303  ordtrestNEW  34311  ordtrest2NEWlem  34312  fnrelpredd  35482  fineqvnttrclse  35537  satfv1lem  35854  satefvfmla0  35910  satefvfmla1  35917  lineunray  36639  lineelsb2  36640  linecom  36642  nmulrid  36697  ee7.2aOLD  36972  poimirlem26  38297  poimirlem27  38298  mbfposadd  38318  cnambfre  38319  itg2addnclem2  38323  iblabsnclem  38334  ftc1anclem1  38344  lfl1dim2N  39896  pmapat  40537  pmapglbx  40543  dvhb1dimN  41760  dia0  41826  mapdval2N  42404  mapdsn  42415  hlhilocv  42731  isprimroot  42860  aks6d1c6isolem3  42943  unitscyglem5  42966  istopclsd  43431  diophren  43540  rabrenfdioph  43541  pwfi2f1o  43823  idomodle  43918  hausgraph  43932  nadd1rabtr  44115  nadd1rabex  44117  nadd1suc  44119  minregex2  44261  fsovcnvlem  44739  ntrneifv3  44808  ntrneifv4  44811  clsneifv3  44836  clsneifv4  44837  neicvgfv  44847  nzss  45027  preimaiocmnf  46276  preimaicomnf  47425  smfsupxr  47530  smfliminflem  47544  sprvalpwle2  48238  fpprmod  48492  dfsclnbgr2  48611  dfvopnbgr2  48618  uspgrlimlem2  48754  rmsupp0  49148  lco0  49207  rrxlinesc  49515  rrxlinec  49516  rrx2line  49520  rrx2vlinest  49521  rrx2linest  49522  rrx2linesl  49523  rrx2linest2  49524  2sphere  49529  2sphere0  49530  line2  49532  itsclinecirc0b  49554