Metamath Proof Explorer


Axiom ax-rrecex

Description: Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex . (Contributed by Eric Schmidt, 11-Apr-2007)

Ref Expression
Assertion ax-rrecex A A 0 x A x = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class
2 0 1 wcel wff A
3 cc0 class 0
4 0 3 wne wff A 0
5 2 4 wa wff A A 0
6 vx setvar x
7 cmul class ×
8 6 cv setvar x
9 0 8 7 co class A x
10 c1 class 1
11 9 10 wceq wff A x = 1
12 11 6 1 wrex wff x A x = 1
13 5 12 wi wff A A 0 x A x = 1