Theorem dfcleq 2730

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2709) and the definition of class equality (df-cleq 2729). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2712 to prove also the hypothesis of df-cleq 2729 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1797, equid 2014 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)

Assertion

Ref	Expression
dfcleq	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfcleq

Dummy variables 𝑦 𝑧 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axextb 2712	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2712	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2729	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  cvjust  2731  ax9ALT  2732  eleq2w2  2733  eqriv  2734  eqrdv  2735  eqeq1d  2739  eqeq1dALT  2740  abbib  2806  eqabbw  2810  eleq2d  2823  eleq2dALT  2824  cleqh  2866  nfeqd  2910  cleqf  2928  rexeq  3294  raleqbidvvOLD  3307  rmoeq1  3383  eqv  3452  abv  3454  csbied  3887  dfss2  3921  eqss  3951  ssequn1  4140  eq0ALT  4305  disj3  4408  undif4  4421  intprg  4938  vnex  5261  inex1  5264  axprALT  5369  zfpair2  5380  prex  5384  sucel  6401  uniex2  7693  brtxpsd3  36110  hfext  36399  in-ax8  36440  onsuct0  36657  eliminable2a  37108  eliminable2b  37109  eliminable2c  37110  eliminable-veqab  37114  eliminable-abeqv  37115  eliminable-abeqab  37116  bj-sbeq  37149  bj-sbceqgALT  37150  bj-snsetex  37211  bj-clex  37279  eleq2w2ALT  37295  wl-cleq-0  37750  wl-cleq-1  37751  wl-cleq-2  37752  wl-cleq-3  37753  wl-cleq-4  37754  wl-cleq-5  37755  wl-cleq-6  37756  cover2  37966  releccnveq  38512  abbibw  43035  rp-fakeinunass  43871  intimag  44012  relexp0eq  44057  ntrneik4w  44456  undif3VD  45237  permaxext  45361  uzinico  45919  dvnmul  46301  dvnprodlem3  46306  sge00  46734  sge0resplit  46764  sge0fodjrnlem  46774  hspdifhsp  46974  smfresal  47146  mo0sn  49175