Theorem rabbii 3400

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3402. (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 3399	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rab 3396

This theorem is referenced by:  rabbieq  3403  dfdif3OLD  4063  elneldisj  4337  elnelun  4338  dfepfr  5595  epfrc  5596  fndmdifcom  6971  fniniseg2  6990  uniordint  7729  naddov3  8590  dfoi  9392  kmlem3  10039  alephsuc3  10466  hashbclem  14354  gcdcom  16419  gcdass  16453  lcmcom  16499  lcmass  16520  acsfn0  17561  dfinito2  17905  dftermo2  17906  dfrhm2  20387  lbsextg  21094  dmtopon  22833  fctop2  22915  ordtrest2  23114  qtopres  23608  tsmsfbas  24038  shftmbl  25461  ppiub  27137  rpvmasum  27459  noextendlt  27603  nosepne  27614  nosepdm  27618  nosupbnd2lem1  27649  noinfbnd2lem1  27664  noetasuplem4  27670  umgrislfupgrlem  29095  finsumvtxdg2ssteplem1  29519  clwwlknclwwlkdifnum  29952  clwwlknon2num  30077  dlwwlknondlwlknonf1o  30337  numclwlk1lem1  30341  3unrab  32475  aciunf1  32637  fpwrelmapffslem  32707  constrcbvlem  33760  ordtrest2NEW  33928  unelldsys  34163  rossros  34185  aean  34249  orvcval2  34464  subfacp1lem6  35221  satfv1  35399  itg2addnclem2  37712  scottexf  38208  scott0f  38209  refsymrels2  38602  dfeqvrels2  38625  refrelsredund3  38671  dffunsALTV5  38725  glbconxN  39417  primrootsunit1  42130  primrootsunit  42131  3anrabdioph  42815  3orrabdioph  42816  rexrabdioph  42827  2rexfrabdioph  42829  3rexfrabdioph  42830  4rexfrabdioph  42831  6rexfrabdioph  42832  7rexfrabdioph  42833  elnn0rabdioph  42836  elnnrabdioph  42840  rabren3dioph  42848  rmydioph  43047  rmxdioph  43049  expdiophlem2  43055  onuniintrab  43259  relintab  43616  sqrtcvallem1  43664  uzmptshftfval  44379  binomcxplemdvsum  44388  binomcxp  44390  dvnprod  45987  ovnsubadd  46610  hoidmv1lelem3  46631  hoidmvlelem3  46635  ovolval3  46685  ovolval4lem2  46688  ovolval5lem3  46692  smflimlem4  46812