Theorem bj-termab 32846

Description: Every class can be written as (is equal to) a class abstraction. cvjust 2617 is a special instance of it, but the present proof does not require ax-13 2246, contrary to cvjust 2617. This theorem requires ax-ext 2602, df-clab 2609, df-cleq 2615, df-clel 2618, 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 1482, cab 2608 and statements corresponding to defined class constructors.

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

Assertion

Ref	Expression
bj-termab	|- A = { x | x e. A }

Distinct variable group:   x, A

Proof of Theorem bj-termab

Step	Hyp	Ref	Expression
1		biid 251	. 2 |- ( x e. A <-> x e. A )
2	1	bj-abbi2i 32776	1 |- A = { x | x e. A }

Syntax hints:   = wceq 1483   e. wcel 1990   {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618

This theorem is referenced by: (None)