Theorem eqcomi 79

Description: Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypotheses

Ref	Expression
eqcomi.1	⊢ A:α
eqcomi.2	⊢ R⊧[A = B]

Assertion

Ref	Expression
eqcomi	⊢ R⊧[B = A]

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		weq 41	. 2 ⊢ = :(α → (α → ∗))
2		eqcomi.1	. . 3 ⊢ A:α
3		eqcomi.2	. . 3 ⊢ R⊧[A = B]
4	2, 3	eqtypi 78	. 2 ⊢ B:α
5	1, 2, 4, 3	dfov1 74	. . 3 ⊢ R⊧(( = A)B)
6	2, 4, 5	eqcomx 52	. 2 ⊢ R⊧(( = B)A)
7	1, 4, 2, 6	dfov2 75	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-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wov 71  ax-eqtypi 77

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  mpbir  87  3eqtr4i  96  3eqtr3i  97  hbth  109  alrimiv  151  dfan2  154  hbct  155  olc  164  orc  165  exlimdv  167  cbvf  179  alrimi  182  exlimd  183  exmid  199  exnal  201  ax8  211  ax9  212  ax10  213