Theorem abbi 2942

Description: Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Assertion

Ref	Expression
abbi	⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})

Proof of Theorem abbi

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hbab1 2814	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
2		hbab1 2814	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜓})
3	1, 2	cleqh 2929	. 2 ⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} ↔ ∀𝑥(𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜓}))
4		abid 2813	. . . 4 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
5		abid 2813	. . . 4 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜓} ↔ 𝜓)
6	4, 5	bibi12i 331	. . 3 ⊢ ((𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜓}) ↔ (𝜑 ↔ 𝜓))
7	6	albii 1920	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜓}) ↔ ∀𝑥(𝜑 ↔ 𝜓))
8	3, 7	bitr2i 268	1 ⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})

Syntax hints:   ↔ wb 198  ∀wal 1656   = wceq 1658   ∈ wcel 2166  {cab 2811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821

This theorem is referenced by:  abbii  2944  abbid  2945  nabbi  3101  rabbi  3331  sbcbi2  3711  absn  4415  iuneq12df  4764  iotabi  6095  uniabio  6096  iotanul  6101  karden  9035  iuneq12daf  29921  bj-cleq  33471  abeq12  34504  elnev  39478  csbingVD  39938  csbsngVD  39947  csbxpgVD  39948  csbrngVD  39950  csbunigVD  39952  csbfv12gALTVD  39953