Theorem eqrd 3622

Description: Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.)

Hypotheses

Ref	Expression
eqrd.0	|- F/ x ph
eqrd.1	|- F/_ x A
eqrd.2	|- F/_ x B
eqrd.3	|- ( ph -> ( x e. A <-> x e. B ) )

Assertion

Ref	Expression
eqrd	|- ( ph -> A = B )

Proof of Theorem eqrd

Step	Hyp	Ref	Expression
1		eqrd.0	. . 3 |- F/ x ph
2		eqrd.3	. . 3 |- ( ph -> ( x e. A <-> x e. B ) )
3	1, 2	alrimi 2082	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
4		eqrd.1	. . 3 |- F/_ x A
5		eqrd.2	. . 3 |- F/_ x B
6	4, 5	cleqf 2790	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
7	3, 6	sylibr 224	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   = wceq 1483   F/wnf 1708   e. wcel 1990   F/_wnfc 2751

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-13 2246  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-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  sniota  5878  dissnlocfin  21332  imasnopn  21493  imasncld  21494  imasncls  21495  blval2  22367  eqri  29315  fimarab  29445  ofpreima  29465  ordtconnlem1  29970  qqhval2  30026  reprdifc  30705  topdifinfindis  33194  icorempt2  33199  isbasisrelowllem1  33203  isbasisrelowllem2  33204  areaquad  37802  rfcnpre1  39178  rfcnpre2  39190