Theorem nfeq 2261

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 2107	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
2		nfnfc.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2247	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
4		nfeq.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2247	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵
6	3, 5	nfbi 1549	. . 3 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)
7	6	nfal 1536	. 2 ⊢ Ⅎ𝑥∀𝑧(𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵)
8	1, 7	nfxfr 1431	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   ↔ wb 104  ∀wal 1310   = wceq 1312  Ⅎwnf 1417   ∈ wcel 1461  Ⅎwnfc 2240

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-cleq 2106  df-clel 2109  df-nfc 2242

This theorem is referenced by:  nfel  2262  nfeq1  2263  nfeq2  2265  nfne  2373  raleqf  2594  rexeqf  2595  reueq1f  2596  rmoeq1f  2597  rabeqf  2645  sbceqg  2983  csbhypf  3002  nfiotadxy  5047  nffn  5175  nffo  5300  fvmptdf  5460  mpteqb  5463  fvmptf  5465  eqfnfv2f  5474  dff13f  5623  ovmpos  5846  ov2gf  5847  ovmpodxf  5848  ovmpodf  5854  eqerlem  6412  sumeq2  11014  fsumadd  11061  txcnp  12276  cnmpt11  12288  cnmpt21  12296  cnmptcom  12303