Theorem rabbidva 3439

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-rab 3433

This theorem is referenced by:  rabbidv  3440  rabeqbidva  3449  rabeqbidvaOLD  3450  rabbi2dva  4233  rabxfrd  5422  seinxp  5771  ordintdif  6435  f1oresrab  7146  onsucmin  7840  suppval1  8189  mptsuppd  8210  naddasslem1  8730  naddasslem2  8731  naddsuc2  8737  cantnflem1  9726  harsucnn  10035  dfinfre  12246  ixxin  13400  mptnn0fsuppr  14036  scshwfzeqfzo  14861  incexc2  15870  smueqlem  16523  gcdass  16580  lcmass  16647  pcneg  16907  ramval  17041  acsfn  17703  monpropd  17784  f1omvdcnv  19476  pmtrmvd  19488  submod  19601  odngen  19609  sylow3lem6  19664  efgsfo  19771  rrgsupp  20717  acsfn1p  20816  rngqiprngimf1  21327  dsmmbas2  21774  dsmmacl  21778  frlmbas  21792  frlmsslss2  21812  mplsubglem2  22038  ltbwe  22079  coe1mul2lem2  22286  scmatmats  22532  mretopd  23115  ordtbaslem  23211  ordtrest  23225  ordtrest2lem  23226  leordtval  23236  xkopt  23678  xkoco1cn  23680  xkoco2cn  23681  xkoinjcn  23710  r0cld  23761  utopsnneiplem  24271  stdbdbl  24545  minveclem3b  25475  minveclem4  25479  lhop1lem  26066  idomrootle  26226  mumul  27238  sqff1o  27239  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1a  27449  lrrecse  27989  lrrecpred  27991  elntg2  29014  edglnl  29174  nbupgr  29375  vtxdun  29513  wwlksnextprop  29941  wpthswwlks2on  29990  rusgrnumwwlkslem  29998  rusgrnumwwlks  30003  clwlknf1oclwwlkn  30112  frcond3  30297  extwwlkfab  30380  grpoidinv2  30543  grpoinv  30553  xppreima  32661  qusker  33356  nsgqusf1olem3  33422  fedgmullem2  33657  ply1annidllem  33708  zarclsun  33830  cnvordtrestixx  33873  ordtrestNEW  33881  ordtrest2NEWlem  33882  fnrelpredd  35081  satfv1lem  35346  satefvfmla0  35402  satefvfmla1  35409  lineunray  36128  lineelsb2  36129  linecom  36131  ee7.2aOLD  36443  poimirlem26  37632  poimirlem27  37633  mbfposadd  37653  cnambfre  37654  itg2addnclem2  37658  iblabsnclem  37669  ftc1anclem1  37679  lfl1dim2N  39103  pmapat  39745  pmapglbx  39751  dvhb1dimN  40968  dia0  41034  mapdval2N  41612  mapdsn  41623  hlhilocv  41943  isprimroot  42074  aks6d1c6isolem3  42157  unitscyglem5  42180  istopclsd  42687  diophren  42800  rabrenfdioph  42801  pwfi2f1o  43084  idomodle  43179  hausgraph  43193  nadd1rabtr  43377  nadd1rabex  43379  nadd1suc  43381  minregex2  43524  fsovcnvlem  44002  ntrneifv3  44071  ntrneifv4  44074  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  nzss  44312  preimaiocmnf  45513  preimaicomnf  46666  smfsupxr  46771  smfliminflem  46785  sprvalpwle2  47413  fpprmod  47651  dfsclnbgr2  47769  dfvopnbgr2  47776  uspgrlimlem2  47891  rmsupp0  48212  lco0  48272  rrxlinesc  48584  rrxlinec  48585  rrx2line  48589  rrx2vlinest  48590  rrx2linest  48591  rrx2linesl  48592  rrx2linest2  48593  2sphere  48598  2sphere0  48599  line2  48601  itsclinecirc0b  48623