Metamath Proof Explorer


Theorem relexpfldd

Description: The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

Ref Expression
Hypothesis relexpfldd.1 φ N 0
Assertion relexpfldd φ R r N R

Proof

Step Hyp Ref Expression
1 relexpfldd.1 φ N 0
2 relexpfld N 0 R V R r N R
3 1 2 sylan φ R V R r N R
4 3 ex φ R V R r N R
5 reldmrelexp Rel dom r
6 5 ovprc1 ¬ R V R r N =
7 6 unieqd ¬ R V R r N =
8 uni0 =
9 7 8 eqtrdi ¬ R V R r N =
10 9 unieqd ¬ R V R r N =
11 10 8 eqtrdi ¬ R V R r N =
12 0ss R
13 11 12 eqsstrdi ¬ R V R r N R
14 4 13 pm2.61d1 φ R r N R