Theorem rabbii 3402

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3404. (Contributed by Peter Mazsa, 1-Nov-2019.)

Hypothesis

Ref	Expression
rabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rabbii	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem rabbii

Step	Hyp	Ref	Expression
1		rabbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rabbiia 3400	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3397

This theorem is referenced by:  rabbieq  3405  dfdif3OLD  4071  elneldisj  4345  elnelun  4346  dfepfr  5607  epfrc  5608  fndmdifcom  6981  fniniseg2  7000  uniordint  7741  naddov3  8605  dfoi  9422  kmlem3  10066  alephsuc3  10493  hashbclem  14377  gcdcom  16442  gcdass  16476  lcmcom  16522  lcmass  16543  acsfn0  17584  dfinito2  17928  dftermo2  17929  dfrhm2  20377  lbsextg  21087  dmtopon  22826  fctop2  22908  ordtrest2  23107  qtopres  23601  tsmsfbas  24031  shftmbl  25455  ppiub  27131  rpvmasum  27453  noextendlt  27597  nosepne  27608  nosepdm  27612  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetasuplem4  27664  umgrislfupgrlem  29085  finsumvtxdg2ssteplem1  29509  clwwlknclwwlkdifnum  29942  clwwlknon2num  30067  dlwwlknondlwlknonf1o  30327  numclwlk1lem1  30331  3unrab  32465  aciunf1  32620  fpwrelmapffslem  32688  constrcbvlem  33724  ordtrest2NEW  33892  unelldsys  34127  rossros  34149  aean  34213  orvcval2  34429  subfacp1lem6  35160  satfv1  35338  itg2addnclem2  37654  scottexf  38150  scott0f  38151  refsymrels2  38544  dfeqvrels2  38567  refrelsredund3  38613  dffunsALTV5  38667  glbconxN  39360  primrootsunit1  42073  primrootsunit  42074  3anrabdioph  42758  3orrabdioph  42759  rexrabdioph  42770  2rexfrabdioph  42772  3rexfrabdioph  42773  4rexfrabdioph  42774  6rexfrabdioph  42775  7rexfrabdioph  42776  elnn0rabdioph  42779  elnnrabdioph  42783  rabren3dioph  42791  rmydioph  42990  rmxdioph  42992  expdiophlem2  42998  onuniintrab  43202  relintab  43559  sqrtcvallem1  43607  uzmptshftfval  44322  binomcxplemdvsum  44331  binomcxp  44333  dvnprod  45934  ovnsubadd  46557  hoidmv1lelem3  46578  hoidmvlelem3  46582  ovolval3  46632  ovolval4lem2  46635  ovolval5lem3  46639  smflimlem4  46759