Theorem nfeq 2382

Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfnfc.1	⊢ Ⅎ𝑥𝐴
nfeq.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq	⊢ Ⅎ𝑥 𝐴 = 𝐵

Proof of Theorem nfeq

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2225	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
2		nfnfc.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2368	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
4		nfeq.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2368	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵
6	3, 5	nfbi 1637	. . 3 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)
7	6	nfal 1624	. 2 ⊢ Ⅎ𝑥∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)
8	1, 7	nfxfr 1522	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   ↔ wb 105  ∀wal 1395   = wceq 1397  Ⅎwnf 1508   ∈ wcel 2202  Ⅎwnfc 2361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363

This theorem is referenced by:  nfel  2383  nfeq1  2384  nfeq2  2386  nfne  2495  raleqf  2726  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  rabeqf  2792  sbceqg  3143  csbhypf  3166  nfiotadw  5289  nffn  5426  nffo  5558  fvmptdf  5734  mpteqb  5737  fvmptf  5739  eqfnfv2f  5748  dff13f  5910  ovmpos  6144  ov2gf  6145  ovmpodxf  6146  ovmpodf  6152  eqerlem  6732  sumeq2  11919  fsumadd  11966  prodeq1f  12112  prodeq2  12117  txcnp  14994  cnmpt11  15006  cnmpt21  15014  cnmptcom  15021  dvmptfsum  15448  lgseisenlem2  15799