Theorem rabbidva 3407

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3401

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3402

This theorem is referenced by:  rabbidv  3408  rabeqbidva  3417  rabeqbidvaOLD  3418  rabbi2dva  4180  rabxfrd  5364  seinxp  5716  ordintdif  6376  f1oresrab  7082  onsucmin  7773  suppval1  8118  mptsuppd  8139  naddasslem1  8632  naddasslem2  8633  naddsuc2  8639  cantnflem1  9610  harsucnn  9922  dfinfre  12135  ixxin  13290  mptnn0fsuppr  13934  scshwfzeqfzo  14761  incexc2  15773  smueqlem  16429  gcdass  16486  lcmass  16553  pcneg  16814  ramval  16948  acsfn  17594  monpropd  17673  f1omvdcnv  19385  pmtrmvd  19397  submod  19510  odngen  19518  sylow3lem6  19573  efgsfo  19680  rrgsupp  20646  acsfn1p  20744  rngqiprngimf1  21267  dsmmbas2  21704  dsmmacl  21708  frlmbas  21722  frlmsslss2  21742  mplsubglem2  21968  ltbwe  22011  coe1mul2lem2  22222  scmatmats  22467  mretopd  23048  ordtbaslem  23144  ordtrest  23158  ordtrest2lem  23159  leordtval  23169  xkopt  23611  xkoco1cn  23613  xkoco2cn  23614  xkoinjcn  23643  r0cld  23694  utopsnneiplem  24203  stdbdbl  24473  minveclem3b  25396  minveclem4  25400  lhop1lem  25986  idomrootle  26146  mumul  27159  sqff1o  27160  lgsquadlem1  27359  lgsquadlem2  27360  2lgslem1a  27370  lrrecse  27950  lrrecpred  27952  elntg2  29070  edglnl  29228  nbupgr  29429  vtxdun  29567  wwlksnextprop  29997  wpthswwlks2on  30049  rusgrnumwwlkslem  30057  rusgrnumwwlks  30062  clwlknf1oclwwlkn  30171  frcond3  30356  extwwlkfab  30439  grpoidinv2  30603  grpoinv  30613  xppreima  32735  qusker  33442  nsgqusf1olem3  33508  fedgmullem2  33808  ply1annidllem  33879  zarclsun  34048  cnvordtrestixx  34091  ordtrestNEW  34099  ordtrest2NEWlem  34100  fnrelpredd  35268  fineqvnttrclse  35302  satfv1lem  35578  satefvfmla0  35634  satefvfmla1  35641  lineunray  36363  lineelsb2  36364  linecom  36366  ee7.2aOLD  36677  poimirlem26  37897  poimirlem27  37898  mbfposadd  37918  cnambfre  37919  itg2addnclem2  37923  iblabsnclem  37934  ftc1anclem1  37944  lfl1dim2N  39498  pmapat  40139  pmapglbx  40145  dvhb1dimN  41362  dia0  41428  mapdval2N  42006  mapdsn  42017  hlhilocv  42333  isprimroot  42463  aks6d1c6isolem3  42546  unitscyglem5  42569  istopclsd  43057  diophren  43170  rabrenfdioph  43171  pwfi2f1o  43453  idomodle  43548  hausgraph  43562  nadd1rabtr  43745  nadd1rabex  43747  nadd1suc  43749  minregex2  43891  fsovcnvlem  44369  ntrneifv3  44438  ntrneifv4  44441  clsneifv3  44466  clsneifv4  44467  neicvgfv  44477  nzss  44673  preimaiocmnf  45920  preimaicomnf  47069  smfsupxr  47174  smfliminflem  47188  sprvalpwle2  47849  fpprmod  48087  dfsclnbgr2  48206  dfvopnbgr2  48213  uspgrlimlem2  48349  rmsupp0  48728  lco0  48787  rrxlinesc  49095  rrxlinec  49096  rrx2line  49100  rrx2vlinest  49101  rrx2linest  49102  rrx2linesl  49103  rrx2linest2  49104  2sphere  49109  2sphere0  49110  line2  49112  itsclinecirc0b  49134