Theorem bj-termab 32039

Description: Every class can be written as (is equal to) a class abstraction. cvjust 2605 is a special instance of it, but the present proof does not require ax-13 2234, contrary to cvjust 2605. This theorem requires ax-ext 2590, df-clab 2597, df-cleq 2603, df-clel 2606, but to prove that any specific class term not containing class variables is a setvar or can be written as (is equal to) a class abstraction does not require these $a-statements. This last fact is a metatheorem, consequence of the fact that the only $a-statements with typecode class are cv 1474, cab 2596 and statements corresponding to defined class constructors.

UPDATE: This theorem is (almost) abid2 2732 and bj-abid2 31970, though the present proof is shorter than a proof from bj-abid2 31970 and eqcomi 2619 (and is shorter than the proof of either); plus, it is of the same form as cvjust 2605 and such a basic statement deserves to be present in both forms. Note that bj-termab 32039 shortens the proof of abid2 2732, and shortens five proofs by a total of 72 bytes. Move it to Main as "abid1" proved from abbi2i 2725? Note also that this is the form in Quine, more than abid2 2732. (Contributed by BJ, 21-Oct-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-termab	⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}

Distinct variable group:   𝑥,𝐴

Proof of Theorem bj-termab

Step	Hyp	Ref	Expression
1		biid 250	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
2	1	bj-abbi2i 31964	1 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}

Syntax hints:   = wceq 1475   ∈ wcel 1977  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606

This theorem is referenced by: (None)