This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Class form not-free predicate nfeq
Description: Hypothesis builder for equality. (Contributed by NM , 21-Jun-1993)
(Revised by Mario Carneiro , 11-Aug-2016) (Proof shortened by Wolf
Lammen , 16-Nov-2019)
Ref
Expression
Hypotheses
nfnfc.1 |- F/_ x A
nfeq.2 |- F/_ x B
Assertion
nfeq |- F/ x A = B
Proof
Step
Hyp
Ref
Expression
1
nfnfc.1 |- F/_ x A
2
nfeq.2 |- F/_ x B
3
1
a1i |- ( T. -> F/_ x A )
4
2
a1i |- ( T. -> F/_ x B )
5
3 4
nfeqd |- ( T. -> F/ x A = B )
6
5
mptru |- F/ x A = B