Axiom ax-leq 69

Description: Equality theorem for abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-leq.1	|- A:be
ax-leq.2	|- B:be
ax-leq.3	|- R |= (( = A)B)

Assertion

Ref	Expression
ax-leq	|- R |= (( = \x:al A)\x:al B)

Distinct variable group:   x,R

Detailed syntax breakdown of Axiom ax-leq

Step	Hyp	Ref	Expression
1		tr	. 2 term R
2		ke 7	. . . 4 term =
3		hal	. . . . 5 type al
4		vx	. . . . 5 var x
5		ta	. . . . 5 term A
6	3, 4, 5	kl 6	. . . 4 term \x:al A
7	2, 6	kc 5	. . 3 term ( = \x:al A)
8		tb	. . . 4 term B
9	3, 4, 8	kl 6	. . 3 term \x:al B
10	7, 9	kc 5	. 2 term (( = \x:al A)\x:al B)
11	1, 10	wffMMJ2 11	1 wff R |= (( = \x:al A)\x:al B)

This axiom is referenced by:  leq  91