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 3398	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

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

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 3395

This theorem is referenced by:  rabbieq  3403  dfdif3OLD  4069  elneldisj  4343  elnelun  4344  dfepfr  5603  epfrc  5604  fndmdifcom  6977  fniniseg2  6996  uniordint  7737  naddov3  8598  dfoi  9403  kmlem3  10047  alephsuc3  10474  hashbclem  14359  gcdcom  16424  gcdass  16458  lcmcom  16504  lcmass  16525  acsfn0  17566  dfinito2  17910  dftermo2  17911  dfrhm2  20359  lbsextg  21069  dmtopon  22808  fctop2  22890  ordtrest2  23089  qtopres  23583  tsmsfbas  24013  shftmbl  25437  ppiub  27113  rpvmasum  27435  noextendlt  27579  nosepne  27590  nosepdm  27594  nosupbnd2lem1  27625  noinfbnd2lem1  27640  noetasuplem4  27646  umgrislfupgrlem  29071  finsumvtxdg2ssteplem1  29495  clwwlknclwwlkdifnum  29928  clwwlknon2num  30053  dlwwlknondlwlknonf1o  30313  numclwlk1lem1  30317  3unrab  32452  aciunf1  32614  fpwrelmapffslem  32684  constrcbvlem  33738  ordtrest2NEW  33906  unelldsys  34141  rossros  34163  aean  34227  orvcval2  34443  subfacp1lem6  35178  satfv1  35356  itg2addnclem2  37672  scottexf  38168  scott0f  38169  refsymrels2  38562  dfeqvrels2  38585  refrelsredund3  38631  dffunsALTV5  38685  glbconxN  39377  primrootsunit1  42090  primrootsunit  42091  3anrabdioph  42775  3orrabdioph  42776  rexrabdioph  42787  2rexfrabdioph  42789  3rexfrabdioph  42790  4rexfrabdioph  42791  6rexfrabdioph  42792  7rexfrabdioph  42793  elnn0rabdioph  42796  elnnrabdioph  42800  rabren3dioph  42808  rmydioph  43007  rmxdioph  43009  expdiophlem2  43015  onuniintrab  43219  relintab  43576  sqrtcvallem1  43624  uzmptshftfval  44339  binomcxplemdvsum  44348  binomcxp  44350  dvnprod  45950  ovnsubadd  46573  hoidmv1lelem3  46594  hoidmvlelem3  46598  ovolval3  46648  ovolval4lem2  46651  ovolval5lem3  46655  smflimlem4  46775