Step 
Hyp 
Ref 
Expression 
1 

ersymb.1 
 ( ph > R Er X ) 
2 

erref.2 
 ( ph > A e. X ) 
3 

erdm 
 ( R Er X > dom R = X ) 
4 
1 3

syl 
 ( ph > dom R = X ) 
5 
2 4

eleqtrrd 
 ( ph > A e. dom R ) 
6 

eldmg 
 ( A e. X > ( A e. dom R <> E. x A R x ) ) 
7 
2 6

syl 
 ( ph > ( A e. dom R <> E. x A R x ) ) 
8 
5 7

mpbid 
 ( ph > E. x A R x ) 
9 
1

adantr 
 ( ( ph /\ A R x ) > R Er X ) 
10 

simpr 
 ( ( ph /\ A R x ) > A R x ) 
11 
9 10 10

ertr4d 
 ( ( ph /\ A R x ) > A R A ) 
12 
8 11

exlimddv 
 ( ph > A R A ) 