Theorem rabbidva 3478

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-rab 3147

This theorem is referenced by:  rabbidv  3480  rabeqbidva  3486  rabbi2dva  4193  rabxfrd  5317  seinxp  5634  ordintdif  6239  f1oresrab  6888  onsucmin  7535  suppval1  7835  mptsuppd  7852  cantnflem1  9151  dfinfre  11621  ixxin  12754  mptnn0fsuppr  13366  scshwfzeqfzo  14187  incexc2  15192  smueqlem  15838  gcdass  15894  lcmass  15957  pcneg  16209  ramval  16343  acsfn  16929  monpropd  17006  f1omvdcnv  18571  pmtrmvd  18583  submod  18693  odngen  18701  sylow3lem6  18756  efgsfo  18864  acsfn1p  19577  rrgsupp  20063  mplsubglem2  20215  ltbwe  20252  mhpinvcl  20338  coe1mul2lem2  20435  dsmmbas2  20880  dsmmacl  20884  frlmbas  20898  frlmsslss2  20918  scmatmats  21119  mretopd  21699  ordtbaslem  21795  ordtrest  21809  ordtrest2lem  21810  leordtval  21820  xkopt  22262  xkoco1cn  22264  xkoco2cn  22265  xkoinjcn  22294  r0cld  22345  utopsnneiplem  22855  stdbdbl  23126  minveclem3b  24030  minveclem4  24034  lhop1lem  24609  mumul  25757  sqff1o  25758  lgsquadlem1  25955  lgsquadlem2  25956  2lgslem1a  25966  elntg2  26770  edglnl  26927  nbupgr  27125  vtxdun  27262  wwlksnextprop  27690  wpthswwlks2on  27739  rusgrnumwwlkslem  27747  rusgrnumwwlks  27752  clwlknf1oclwwlkn  27862  frcond3  28047  extwwlkfab  28130  grpoidinv2  28291  grpoinv  28301  xppreima  30393  qusker  30918  fedgmullem2  31026  cnvordtrestixx  31156  ordtrestNEW  31164  ordtrest2NEWlem  31165  satfv1lem  32609  satefvfmla0  32665  satefvfmla1  32672  lineunray  33608  lineelsb2  33609  linecom  33611  ee7.2aOLD  33809  poimirlem26  34917  poimirlem27  34918  mbfposadd  34938  cnambfre  34939  itg2addnclem2  34943  iblabsnclem  34954  ftc1anclem1  34966  lfl1dim2N  36257  pmapat  36898  pmapglbx  36904  dvhb1dimN  38121  dia0  38187  mapdval2N  38765  mapdsn  38776  hlhilocv  39092  istopclsd  39295  diophren  39408  rabrenfdioph  39409  pwfi2f1o  39694  idomrootle  39793  idomodle  39794  hausgraph  39810  harsucnn  39901  fsovcnvlem  40357  ntrneifv3  40430  ntrneifv4  40433  clsneifv3  40458  clsneifv4  40459  neicvgfv  40469  nzss  40647  preimaiocmnf  41835  preimaicomnf  42989  smfsupxr  43089  smfliminflem  43103  sprvalpwle2  43650  fpprmod  43891  rmsupp0  44415  lco0  44481  rrxlinesc  44721  rrxlinec  44722  rrx2line  44726  rrx2vlinest  44727  rrx2linest  44728  rrx2linesl  44729  rrx2linest2  44730  2sphere  44735  2sphere0  44736  line2  44738  itsclinecirc0b  44760