Theorem eqcomi 70

Description: Commutativity of equality.

Hypotheses

Ref	Expression
eqcomi.1	|- A:al
eqcomi.2	|- R |= [A = B]

Assertion

Ref	Expression
eqcomi	|- R |= [B = A]

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		weq 38	. 2 |- = :(al -> (al -> *))
2		eqcomi.1	. . 3 |- A:al
3		eqcomi.2	. . 3 |- R |= [A = B]
4	2, 3	eqtypi 69	. 2 |- B:al
5	1, 2, 4, 3	dfov1 66	. . 3 |- R |= (( = A)B)
6	2, 4, 5	eqcomx 47	. 2 |- R |= (( = B)A)
7	1, 4, 2, 6	dfov2 67	1 |- R |= [B = A]

Syntax hints:   = 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-refl 39  ax-eqmp 42  ax-ceq 46

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  mpbir  77  3eqtr4i  86  3eqtr3i  87  hbth  99  alrimiv  141  dfan2  144  hbct  145  olc  154  orc  155  exlimdv  157  cbvf  167  alrimi  170  exlimd  171  exmid  186  exnal  188  ax8  198  ax9  199  ax10  200