Theorem rabbii 3408

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

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

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 3403

This theorem is referenced by:  rabbieq  3411  dfdif3OLD  4077  elneldisj  4351  elnelun  4352  dfepfr  5615  epfrc  5616  fndmdifcom  6997  fniniseg2  7016  uniordint  7757  naddov3  8621  dfoi  9440  kmlem3  10082  alephsuc3  10509  hashbclem  14393  gcdcom  16459  gcdass  16493  lcmcom  16539  lcmass  16560  acsfn0  17597  dfinito2  17941  dftermo2  17942  dfrhm2  20359  lbsextg  21048  dmtopon  22786  fctop2  22868  ordtrest2  23067  qtopres  23561  tsmsfbas  23991  shftmbl  25415  ppiub  27091  rpvmasum  27413  noextendlt  27557  nosepne  27568  nosepdm  27572  nosupbnd2lem1  27603  noinfbnd2lem1  27618  noetasuplem4  27624  umgrislfupgrlem  29025  finsumvtxdg2ssteplem1  29449  clwwlknclwwlkdifnum  29882  clwwlknon2num  30007  dlwwlknondlwlknonf1o  30267  numclwlk1lem1  30271  3unrab  32405  aciunf1  32560  fpwrelmapffslem  32628  constrcbvlem  33718  ordtrest2NEW  33886  unelldsys  34121  rossros  34143  aean  34207  orvcval2  34423  subfacp1lem6  35145  satfv1  35323  itg2addnclem2  37639  scottexf  38135  scott0f  38136  refsymrels2  38529  dfeqvrels2  38552  refrelsredund3  38598  dffunsALTV5  38652  glbconxN  39345  primrootsunit1  42058  primrootsunit  42059  3anrabdioph  42743  3orrabdioph  42744  rexrabdioph  42755  2rexfrabdioph  42757  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  elnn0rabdioph  42764  elnnrabdioph  42768  rabren3dioph  42776  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  onuniintrab  43188  relintab  43545  sqrtcvallem1  43593  uzmptshftfval  44308  binomcxplemdvsum  44317  binomcxp  44319  dvnprod  45920  ovnsubadd  46543  hoidmv1lelem3  46564  hoidmvlelem3  46568  ovolval3  46618  ovolval4lem2  46621  ovolval5lem3  46625  smflimlem4  46745