Theorem rabbidva 3410

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109  {crab 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-rab 3074

This theorem is referenced by:  rabbidv  3412  rabeqbidva  3419  rabbi2dva  4156  rabxfrd  5343  seinxp  5669  ordintdif  6312  f1oresrab  6993  onsucmin  7656  suppval1  7967  mptsuppd  7987  cantnflem1  9408  harsucnn  9740  dfinfre  11939  ixxin  13078  mptnn0fsuppr  13700  scshwfzeqfzo  14520  incexc2  15531  smueqlem  16178  gcdass  16236  lcmass  16300  pcneg  16556  ramval  16690  acsfn  17349  monpropd  17430  f1omvdcnv  19033  pmtrmvd  19045  submod  19155  odngen  19163  sylow3lem6  19218  efgsfo  19326  acsfn1p  20048  rrgsupp  20543  dsmmbas2  20925  dsmmacl  20929  frlmbas  20943  frlmsslss2  20963  mplsubglem2  21188  ltbwe  21226  coe1mul2lem2  21420  scmatmats  21641  mretopd  22224  ordtbaslem  22320  ordtrest  22334  ordtrest2lem  22335  leordtval  22345  xkopt  22787  xkoco1cn  22789  xkoco2cn  22790  xkoinjcn  22819  r0cld  22870  utopsnneiplem  23380  stdbdbl  23654  minveclem3b  24573  minveclem4  24577  lhop1lem  25158  mumul  26311  sqff1o  26312  lgsquadlem1  26509  lgsquadlem2  26510  2lgslem1a  26520  elntg2  27334  edglnl  27494  nbupgr  27692  vtxdun  27829  wwlksnextprop  28256  wpthswwlks2on  28305  rusgrnumwwlkslem  28313  rusgrnumwwlks  28318  clwlknf1oclwwlkn  28427  frcond3  28612  extwwlkfab  28695  grpoidinv2  28856  grpoinv  28866  xppreima  30962  qusker  31528  nsgqusf1olem3  31579  fedgmullem2  31690  zarclsun  31799  cnvordtrestixx  31842  ordtrestNEW  31850  ordtrest2NEWlem  31851  fnrelpredd  33040  satfv1lem  33303  satefvfmla0  33359  satefvfmla1  33366  lrrecse  34078  lrrecpred  34080  lineunray  34428  lineelsb2  34429  linecom  34431  ee7.2aOLD  34629  poimirlem26  35782  poimirlem27  35783  mbfposadd  35803  cnambfre  35804  itg2addnclem2  35808  iblabsnclem  35819  ftc1anclem1  35829  lfl1dim2N  37115  pmapat  37756  pmapglbx  37762  dvhb1dimN  38979  dia0  39045  mapdval2N  39623  mapdsn  39634  hlhilocv  39954  istopclsd  40502  diophren  40615  rabrenfdioph  40616  pwfi2f1o  40901  idomrootle  41000  idomodle  41001  hausgraph  41017  fsovcnvlem  41574  ntrneifv3  41645  ntrneifv4  41648  clsneifv3  41673  clsneifv4  41674  neicvgfv  41684  nzss  41888  preimaiocmnf  43053  preimaicomnf  44200  smfsupxr  44300  smfliminflem  44314  sprvalpwle2  44893  fpprmod  45131  rmsupp0  45656  lco0  45720  rrxlinesc  46033  rrxlinec  46034  rrx2line  46038  rrx2vlinest  46039  rrx2linest  46040  rrx2linesl  46041  rrx2linest2  46042  2sphere  46047  2sphere0  46048  line2  46050  itsclinecirc0b  46072