Theorem leq 91

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

Hypotheses

Ref	Expression
leq.1	|- A:be
leq.2	|- R |= [A = B]

Assertion

Ref	Expression
leq	|- R |= [\x:al A = \x:al B]

Distinct variable group:   x,R

Proof of Theorem leq

Step	Hyp	Ref	Expression
1		weq 41	. 2 |- = :((al -> be) -> ((al -> be) -> *))
2		leq.1	. . 3 |- A:be
3	2	wl 66	. 2 |- \x:al A:(al -> be)
4		leq.2	. . . 4 |- R |= [A = B]
5	2, 4	eqtypi 78	. . 3 |- B:be
6	5	wl 66	. 2 |- \x:al B:(al -> be)
7		weq 41	. . . 4 |- = :(be -> (be -> *))
8	7, 2, 5, 4	dfov1 74	. . 3 |- R |= (( = A)B)
9	2, 5, 8	ax-leq 69	. 2 |- R |= (( = \x:al A)\x:al B)
10	1, 3, 6, 9	dfov2 75	1 |- R |= [\x:al A = \x:al B]

Syntax hints:   -> ht 2  \kl 6   = ke 7  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wl 65  ax-leq 69  ax-wov 71  ax-eqtypi 77

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  hbxfrf  107  hbl  112  exval  143  euval  144  orval  147  anval  148  alrimiv  151  dfan2  154  olc  164  orc  165  exlimdv2  166  eta  178  cbvf  179  leqf  181  exlimd  183  ac  197  exmid  199  exnal  201  axpow  221  axun  222